Commit 2024-05-18 08:22 0bd43a90

View on Github →

chore(RingTheory/Polynomial): rename frange to coeffs (#12919) Renames Polynomial.frange to Polynomial.coeffs.

Estimated changes

added theorem Polynomial.coeffs_one
added theorem Polynomial.coeffs_zero
deleted def Polynomial.frange
deleted theorem Polynomial.frange_one
deleted theorem Polynomial.frange_zero
deleted theorem Polynomial.mem_frange_iff
modified def Polynomial.toSubring
modified theorem Polynomial.toSubring_zero