Commit 2024-05-22 00:03 81d68783

View on Github →

chore: tidy various files (#13056)

Estimated changes

Modified Mathlib/Algebra/Exact.lean

Modified Mathlib/Algebra/Module/Injective.lean

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Enough.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

Modified Mathlib/Data/Finset/Sigma.lean

Modified Mathlib/Data/Nat/Interval.lean

Modified Mathlib/Data/Real/ConjExponents.lean

Modified Mathlib/Data/Real/Sqrt.lean

modified theorem Real.real_sqrt_le_nat_sqrt_succ

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Data/ZMod/Quotient.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

modified theorem Measurable.map_measurableSpace_eq

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Polynomial/Vieta.lean

Modified Mathlib/Topology/Perfect.lean

Modified Mathlib/Topology/TietzeExtension.lean