Commit 2026-01-05 08:11 8fedec2a

View on Github →

chore: golf proofs (#33541)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/LinearAlgebra/Ray.lean

modified theorem SameRay.refl

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Modified Mathlib/RingTheory/Trace/Defs.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean