Commit 2026-05-20 21:42 ae5f1c03

View on Github →

chore: fix naming of coeff_C_ne_zero (#39632) Split off from #39623

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

deleted theorem Polynomial.coeff_C_ne_zero

added theorem Polynomial.coeff_C_of_ne_zero

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

Modified Mathlib/RingTheory/HahnSeries/HEval.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.coeff_C_of_ne_zero

deleted theorem PowerSeries.coeff_ne_zero_C