Polynomial.coeff_isUnit_isNilpotent_of_isUnit
theorem Polynomial.coeff_isUnit_isNilpotent_of_isUnit :
∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
IsUnit P → IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
The theorem `Polynomial.coeff_isUnit_isNilpotent_of_isUnit` states the following: Given a commutative ring `R` and a polynomial `P` over `R`, if `P` is a unit (meaning there exists another polynomial which when multiplied with `P` gives the multiplicative identity), then two conditions hold. First, the constant term of the polynomial (the coefficient of the degree zero term) is also a unit. Second, all the other coefficients of the polynomial are nilpotent, which means that for each such coefficient, there exists a natural number `n` such that raising the coefficient to the `n`-th power gives zero. This applies to all coefficients except the constant term.
More concisely: Given a commutative ring and a polynomial over it, if the polynomial is a unit, then its constant term is a unit and all other coefficients are nilpotent.
|
Polynomial.isUnit_iff_coeff_isUnit_isNilpotent
theorem Polynomial.isUnit_iff_coeff_isUnit_isNilpotent :
∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
The theorem states that for any commutative ring `R` and any polynomial `P` over `R`, `P` is a unit (i.e., it has a multiplicative inverse in the ring of polynomials) if and only if all its coefficients are nilpotent (i.e., some power of them equals zero) except for the constant term, which must be a unit in `R`. In other words, a polynomial is a unit exactly when its constant term is a unit and all its other coefficients, when raised to some power, give zero.
More concisely: A polynomial over a commutative ring is a unit if and only if its constant term is a unit and all its other coefficients are nilpotent.
|
Polynomial.isUnit_of_coeff_isUnit_isNilpotent
theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent :
∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → IsUnit P
The theorem `Polynomial.isUnit_of_coeff_isUnit_isNilpotent` states that if `P` is a polynomial over a commutative ring `R`, then `P` is a unit under two conditions: First, the constant term of `P` (the coefficient of the power 0) is a unit, meaning it has a two-sided inverse in the ring. Second, all other coefficients of `P` (for all nonzero powers) are nilpotent, which means there exists a natural number for each such coefficient such that raising the coefficient to that power results in zero.
More concisely: If a polynomial `P` over a commutative ring `R` has a unit constant term and all nonconstant coefficients are nilpotent, then `P` is a unit in `R`.
|