Algebraic properties of dual numbers

Main results

• DualNumber.instLocalRing: The dual numbers over a field K form a local ring.
• DualNumber.instPrincipalIdealRing: The dual numbers over a field K form a principal ideal ring.

theorem TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M} : IsNilpotent x ↔ IsNilpotent x.fst

@[simp]

theorem TrivSqZeroExt.isNilpotent_inl_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (r : R) : IsNilpotent (TrivSqZeroExt.inl r) ↔ IsNilpotent r

@[simp]

theorem TrivSqZeroExt.isNilpotent_inr {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : M) : IsNilpotent (TrivSqZeroExt.inr x)

theorem TrivSqZeroExt.isUnit_or_isNilpotent_of_isMaximal_isNilpotent {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] (h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I) (a : TrivSqZeroExt R M) : IsUnit a ∨ IsNilpotent a

theorem TrivSqZeroExt.isUnit_or_isNilpotent {R : Type u_1} {M : Type u_2} [DivisionSemiring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (a : TrivSqZeroExt R M) : IsUnit a ∨ IsNilpotent a

theorem DualNumber.fst_eq_zero_iff_eps_dvd {R : Type u_1} [Semiring R] {x : DualNumber R} : TrivSqZeroExt.fst x = 0 ↔ DualNumber.eps ∣ x

theorem DualNumber.isNilpotent_eps {R : Type u_1} [Semiring R] : IsNilpotent DualNumber.eps

theorem DualNumber.isNilpotent_iff_eps_dvd {R : Type u_1} [DivisionSemiring R] {x : DualNumber R} : IsNilpotent x ↔ DualNumber.eps ∣ x

instance DualNumber.instIsLocalRing {K : Type u_2} [DivisionRing K] : IsLocalRing (DualNumber K)

theorem DualNumber.ideal_trichotomy {K : Type u_2} [DivisionRing K] (I : Ideal (DualNumber K)) : I = ⊥ ∨ I = Ideal.span {DualNumber.eps} ∨ I = ⊤

theorem DualNumber.isMaximal_span_singleton_eps {K : Type u_2} [DivisionRing K] : (Ideal.span {DualNumber.eps}).IsMaximal

theorem DualNumber.maximalIdeal_eq_span_singleton_eps {K : Type u_2} [Field K] : IsLocalRing.maximalIdeal (DualNumber K) = Ideal.span {DualNumber.eps}

instance DualNumber.instIsPrincipalIdealRing {K : Type u_2} [DivisionRing K] : IsPrincipalIdealRing (DualNumber K)

theorem DualNumber.exists_mul_left_or_mul_right {K : Type u_2} [DivisionRing K] (a b : DualNumber K) : ∃ (c : DualNumber K), a * c = b ∨ b * c = a