Commit 2021-08-25 18:32 301eb10e

View on Github →

feat(data/polynomial/monic): monic.is_regular (#8679) This golfs/generalizes some proofs. Additionally, provide some helper API for is_regular, for non-zeros in domains, and for smul of units.

Estimated changes

Modified src/algebra/regular/smul.lean

added theorem is_smul_regular_of_group

modified theorem units.is_smul_regular

Modified src/algebra/ring/basic.lean

Modified src/data/polynomial/monic.lean

deleted theorem polynomial.degree_smul_of_non_zero_divisor

added theorem polynomial.degree_smul_of_smul_regular

deleted theorem polynomial.leading_coeff_smul_of_non_zero_divisor

added theorem polynomial.leading_coeff_smul_of_smul_regular

added theorem polynomial.monic.is_regular

deleted theorem polynomial.nat_degree_smul_of_non_zero_divisor

added theorem polynomial.nat_degree_smul_of_smul_regular