Theorems · Definition · commutative algebra
DualNumber
Type u_4 → Type u_4
The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.
R[ε] is notation for DualNumber R.
- Defined in
- Mathlib.Algebra.DualNumber
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TrivSqZeroExtproof · cited by 180
Cited by57
Results whose statement or proof uses this declaration.
- DualNumber.epsstatement · cited by 30
- Quaternion.dualNumberEquivstatement and proof · cited by 16
- DualNumber.liftstatement · cited by 9
- DualNumber.commute_eps_leftstatement and proof · cited by 3
- DualNumber.inr_eq_smul_epsstatement · cited by 3
- DualNumber.lift_apply_inlstatement · cited by 3
- CliffordAlgebraDualNumber.equivstatement · cited by 2
- Matrix.dualNumberEquivstatement and proof · cited by 2
- DualNumber.algHom_extstatement and proof · cited by 2
- DualNumber.algHom_ext'statement and proof · cited by 2
- DualNumber.eps_mul_epsstatement · cited by 2
- DualNumber.isNilpotent_iff_eps_dvdstatement and proof · cited by 2