Commit 2026-09-28 20:54 f6090c70

View on Github →

chore: rename nonzeroDivisors to nonZeroDivisors in declaration names (#44291) Rename the six lemmas spelling nonZeroDivisors as nonzeroDivisors.

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.X_mem_nonZeroDivisors

deleted theorem Polynomial.X_mem_nonzeroDivisors

added theorem Polynomial.mem_nonZeroDivisors_of_coeff_mem

deleted theorem Polynomial.mem_nonzeroDivisors_of_coeff_mem

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

Modified Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

added theorem MvPowerSeries.X_mem_nonZeroDivisors

deleted theorem MvPowerSeries.X_mem_nonzeroDivisors

added theorem MvPowerSeries.monomial_mem_nonZeroDivisors

added theorem MvPowerSeries.monomial_mem_nonZeroDivisorsLeft

added theorem MvPowerSeries.monomial_mem_nonZeroDivisorsRight

deleted theorem MvPowerSeries.monomial_mem_nonzeroDivisors

deleted theorem MvPowerSeries.monomial_mem_nonzeroDivisorsLeft

deleted theorem MvPowerSeries.monomial_mem_nonzeroDivisorsRight