Commit 2023-08-10 19:52 c4190b46

View on Github →

feat: lemmas about nilpotency and polynomials (#6450)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Regular/Basic.lean

added theorem IsLeftRegular.mul_left_eq_zero_iff

added theorem IsRightRegular.mul_right_eq_zero_iff

Modified Mathlib/Data/Nat/SuccPred.lean

added theorem Nat.forall_ne_zero_iff

Modified Mathlib/Data/Polynomial/Basic.lean

added theorem Polynomial.coeff_C_succ

Modified Mathlib/Data/Polynomial/Coeff.lean

modified theorem Polynomial.coeff_X_pow_self

added theorem Polynomial.isRegular_X

added theorem Polynomial.isRegular_X_pow

deleted theorem Polynomial.mul_X_injective

deleted theorem Polynomial.mul_X_pow_injective

Modified Mathlib/Data/Polynomial/Laurent.lean

Modified Mathlib/Data/Polynomial/Reverse.lean

added theorem Polynomial.revAt_eq_self_of_lt

Created Mathlib/GroupTheory/Submonoid/ZeroDivisors.lean

added theorem coe_nonZeroDivisorsLeft_eq

added theorem coe_nonZeroDivisorsRight_eq

added theorem mem_nonZeroDivisorsLeft_iff

added theorem mem_nonZeroDivisorsRight_iff

added def nonZeroDivisorsLeft

added theorem nonZeroDivisorsLeft_eq_right

added def nonZeroDivisorsRight

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem SuccOrder.forall_ne_bot_iff

Modified Mathlib/RingTheory/Nilpotent.lean

modified theorem IsNilpotent.zero

added theorem isNilpotent_sum

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Polynomial.IsNilpotent.C_mul_X_pow_isNilpotent

deleted theorem Polynomial.coeff_isUnit_isNilpotent_of_isUnit

deleted theorem Polynomial.isUnit_iff_coeff_isUnit_isNilpotent

deleted theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent

Created Mathlib/RingTheory/Polynomial/Nilpotent.lean

added theorem Polynomial.coeff_isUnit_isNilpotent_of_isUnit

added theorem Polynomial.isNilpotent_C_iff

added theorem Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent

added theorem Polynomial.isNilpotent_X_mul_iff

added theorem Polynomial.isNilpotent_monomial_iff

added theorem Polynomial.isNilpotent_mul_X_iff

added theorem Polynomial.isNilpotent_pow_X_mul_C_of_isNilpotent

added theorem Polynomial.isNilpotent_reverse_iff

added theorem Polynomial.isUnit_C_add_X_mul_iff

added theorem Polynomial.isUnit_iff'

added theorem Polynomial.isUnit_iff_coeff_isUnit_isNilpotent

added theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent