Commit 2026-01-21 17:08 a77a2285

View on Github →

chore(Algebra): rename IsRegular_of_ne_zero to IsRegular.of_ne_zero (#34206)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Regular.lean

added theorem IsRegular.of_ne_zero

deleted theorem isRegular_of_ne_zero

Modified Mathlib/Algebra/Module/Torsion/Free.lean

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Polynomial/Sequence.lean

Modified Mathlib/Algebra/Regular/Basic.lean

Modified Mathlib/Algebra/Ring/Regular.lean

added theorem IsRegular.of_ne_zero'

deleted theorem isRegular_of_ne_zero'

Modified Mathlib/Analysis/Polynomial/CauchyBound.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

Modified scripts/nolints_prime_decls.txt