Commit 2026-10-13 18:30 0e03ac81

View on Github →

refactor(RingTheory/PowerSeries/NoZeroDivisors): fix names (#44692) We change e.g. X_prime to prime_X, as per the naming conventions. We also deprecate span_X_isPrime as a trivial consequence of prime_X.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Division.lean

deleted theorem MvPolynomial.X_prime

added theorem MvPolynomial.prime_X

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/PowerSeries/Ideal.lean

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

modified theorem PowerSeries.hasUnitMulPowIrreducibleFactorization

Modified Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean

deleted theorem PowerSeries.X_irreducible

deleted theorem PowerSeries.X_prime

added theorem PowerSeries.irreducible_X

added theorem PowerSeries.prime_X

modified theorem PowerSeries.span_X_isPrime