Commit 2025-09-13 10:43 1fb0e537

View on Github →

chore: tidy various files (#29583)

Estimated changes

Modified Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

Modified Mathlib/Algebra/GroupWithZero/Action/Hom.lean

Modified Mathlib/Algebra/GroupWithZero/Range.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

Modified Mathlib/Algebra/Order/Module/Archimedean.lean

Modified Mathlib/Algebra/QuadraticAlgebra.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Pi.lean

modified theorem List.mem_pi

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Factorial/NatCast.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/Adjoin/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

Modified Mathlib/RingTheory/DividedPowers/RatAlgebra.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Content.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/Topology/Order/IsNormal.lean