Commit 2024-01-17 22:12 a94a9fd8

View on Github →

chore: tidy various files (#9728)

Estimated changes

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/CharP/ExpChar.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

modified theorem CochainComplex.HomComplex.δ_units_smul

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Calculus/Monotone.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

Modified Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Nat/Choose/Basic.lean

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

modified theorem Nat.ascFactorial_eq_div

Modified Mathlib/FieldTheory/Extension.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

deleted theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_IsCancelMulZero

added theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

Modified Mathlib/RingTheory/Binomial.lean

modified def Int.multichoose

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

Modified Mathlib/RingTheory/Localization/Module.lean

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

modified theorem ContinuousMap.coe_mabs

modified theorem ContinuousMap.mabs_apply

Modified test/ApplyAt.lean