Documentation Verification Report

DualNumber

📁 Source: MathlibTest/DualNumber.lean

Statistics

MetricCount
DefinitionsDualNumber
1
Theorems0
Total1

(root)

Definitions

NameCategoryTheorems
DualNumber 📖CompOp
49 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, DualNumber.range_lift, CliffordAlgebraDualNumber.equiv_symm_eps, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.imJ_fst_dualNumberEquiv, Quaternion.imI_fst_dualNumberEquiv, DualNumber.lift_apply_eps, DualNumber.inv_eps, Quaternion.fst_imK_dualNumberEquiv_symm, DualNumber.fst_eq_zero_iff_eps_dvd, DualNumber.maximalIdeal_eq_span_singleton_eps, DualNumber.lift_inlAlgHom_eps, DualNumber.isNilpotent_iff_eps_dvd, DualNumber.isMaximal_span_singleton_eps, DualNumber.lift_smul, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, DualNumber.exists_mul_left_or_mul_right, Quaternion.fst_imJ_dualNumberEquiv_symm, Matrix.dualNumberEquiv_symm_apply, DualNumber.exp_eps, Quaternion.fst_imI_dualNumberEquiv_symm, DualNumber.lift_apply_apply, DualNumber.coe_lift_symm_apply, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, DualNumber.range_inlAlgHom_sup_adjoin_eps, DualNumber.commute_eps_left, DualNumber.algHom_ext_iff, CliffordAlgebraDualNumber.equiv_ι, DualNumber.commute_eps_right, DualNumber.instIsLocalRing, Matrix.dualNumberEquiv_apply, Quaternion.re_snd_dualNumberEquiv, DualNumber.exp_smul_eps, Quaternion.snd_imI_dualNumberEquiv_symm, DualNumber.lift_apply_inl, DualNumber.lift_op_smul, DualNumber.lift_comp_inlHom, DualNumber.algHom_ext'_iff, DualNumber.ideal_trichotomy, DualNumber.inr_eq_smul_eps, DualNumber.eps_mul_eps, DualNumber.snd_mul, DualNumber.instIsPrincipalIdealRing, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, DualNumber.isNilpotent_eps, Quaternion.imK_snd_dualNumberEquiv

---

← Back to Index