Documentation

Mathlib.RingTheory.DualNumber

Algebraic properties of dual numbers #

Main results #

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) :
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)