Commit 2023-03-19 06:49 feb30eae

View on Github →

feat: port Algebra.DualNumber (#2987)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DualNumber.lean

added theorem DualNumber.algHom_ext

added def DualNumber.eps

added theorem DualNumber.eps_mul_eps

added theorem DualNumber.fst_eps

added theorem DualNumber.inr_eq_smul_eps

added def DualNumber.lift

added theorem DualNumber.lift_apply_eps

added theorem DualNumber.lift_eps

added theorem DualNumber.snd_eps

added theorem DualNumber.snd_mul