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 (MulOpposite R) M] [SMulCommClass R (MulOpposite R) M] {x : TrivSqZeroExt R M} : Iff (IsNilpotent x) (IsNilpotent x.fst)

theorem TrivSqZeroExt.isNilpotent_inl_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module (MulOpposite R) M] [SMulCommClass R (MulOpposite R) M] (r : R) : Iff (IsNilpotent (inl r)) (IsNilpotent r)

theorem TrivSqZeroExt.isNilpotent_inr {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module (MulOpposite R) M] [SMulCommClass R (MulOpposite R) M] (x : M) : IsNilpotent (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 (MulOpposite R) M] [IsCentralScalar R M] (h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I) (a : TrivSqZeroExt R M) : Or (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 (MulOpposite R) M] [SMulCommClass R (MulOpposite R) M] (a : TrivSqZeroExt R M) : Or (IsUnit a) (IsNilpotent a)

theorem DualNumber.fst_eq_zero_iff_eps_dvd {R : Type u_1} [Semiring R] {x : DualNumber R} : Iff (Eq (TrivSqZeroExt.fst x) 0) (Dvd.dvd eps x)

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

theorem DualNumber.isNilpotent_iff_eps_dvd {R : Type u_1} [DivisionSemiring R] {x : DualNumber R} : Iff (IsNilpotent x) (Dvd.dvd eps x)

theorem 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)) : Or (Eq I Bot.bot) (Or (Eq I (Ideal.span (Singleton.singleton eps))) (Eq I Top.top))

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

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

theorem 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) : Exists fun (c : DualNumber K) => Or (Eq (HMul.hMul a c) b) (Eq (HMul.hMul b c) a)