Commit 2025-04-15 04:56 7daf90f2

View on Github →

chore: tidy various files (#24052)

Estimated changes

Modified Archive/Imo/Imo2024Q5.lean

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

Modified Mathlib/Algebra/Group/Hom/CompTypeclasses.lean

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

Modified Mathlib/Algebra/PresentedMonoid/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Data/Nat/Dist.lean

modified theorem Nat.dist_pos_of_ne

Modified Mathlib/Data/Real/Cardinality.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/Real.lean

Modified Mathlib/Order/Filter/Bases/Basic.lean

Modified Mathlib/Order/Interval/Set/Union.lean

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Probability/Kernel/Disintegration/Unique.lean

Modified Mathlib/RingTheory/Extension.lean

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

Modified Mathlib/Tactic/FunProp/Decl.lean

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

Modified Mathlib/Topology/UniformSpace/Ascoli.lean