| Metric | Count |
|---|
Definitionsadd, addCommGroup, addCommMonoid, addCommSemigroup, addGroup, addGroupWithOne, addMonoid, addMonoidWithOne, addSemigroup, addZeroClass, algebra', algebraBase, commMonoid, commRing, commSemiring, distribMulAction, fst, fstHom, inhabited, inl, inlAlgHom, inlHom, inr, inrHom, instAlgebra, instInv, instPowNatOfDistribMulActionMulOpposite, invertibleEquivInvertibleFst, invertibleFstOfInvertible, invertibleOfInvertibleFst, liftEquiv, liftEquivOfComm, map, monoid, mul, mulAction, mulOneClass, neg, nonAssocRing, nonAssocSemiring, one, semiring, smul, snd, sndHom, sub, zero | 47 |
TheoremsalgHom_ext, algHom_ext', algHom_ext'_iff, algebraMap_eq_inl, algebraMap_eq_inl', algebraMap_eq_inlHom, ext, ext_iff, fstHom_apply, fstHom_comp_map, fst_add, fst_comp_inl, fst_comp_inr, fst_inl, fst_inr, fst_intCast, fst_inv, fst_invOf, fst_list_prod, fst_map, fst_mk, fst_mul, fst_natCast, fst_neg, fst_one, fst_pow, fst_smul, fst_sub, fst_sum, fst_surjective, fst_zero, ind, inlAlgHom_apply, inlHom_apply, inl_add, inl_fst_add_inr_snd_eq, inl_injective, inl_intCast, inl_mul, inl_mul_eq_smul, inl_mul_inl, inl_mul_inr, inl_natCast, inl_neg, inl_one, inl_pow, inl_smul, inl_sub, inl_sum, inl_zero, inrHom_apply, inr_add, inr_injective, inr_mul_inl, inr_mul_inr, inr_neg, inr_smul, inr_sub, inr_sum, inr_zero, instIsScalarTower, instNontrivial_of_left, instNontrivial_of_right, invOf_eq_inv, inv_inl, inv_inr, inv_inv, inv_mul_cancel, inv_neg, inv_one, inv_zero, invertibleEquivInvertibleFst_apply_invOf, invertibleEquivInvertibleFst_symm_apply_invOf, isCentralScalar, isScalarTower, isUnit_iff_isUnit_fst, isUnit_inl_iff, isUnit_inr_iff, isUnit_inv_iff, liftEquivOfComm_apply, liftEquivOfComm_symm_apply_coe, liftEquiv_apply, liftEquiv_symm_apply_coe, lift_apply_inl, lift_apply_inr, lift_comp_inlHom, lift_comp_inrHom, lift_def, lift_inlAlgHom_inrHom, linearMap_ext, map_comp_inlAlgHom, map_comp_inrHom, map_comp_map, map_id, map_inl, map_inr, mul_inl_eq_op_smul, mul_inv_cancel, mul_inv_rev, mul_left_eq_one, mul_right_eq_one, range_inlAlgHom_sup_adjoin_range_inr, range_liftAux, smulCommClass, sndHom_apply, sndHom_comp_map, snd_add, snd_comp_inl, snd_comp_inr, snd_inl, snd_inr, snd_intCast, snd_inv, snd_invOf, snd_list_prod, snd_map, snd_mk, snd_mul, snd_natCast, snd_neg, snd_one, snd_pow, snd_pow_eq_sum, snd_pow_of_smul_comm, snd_pow_of_smul_comm', snd_smul, snd_sub, snd_sum, snd_surjective, snd_zero | 130 |
| Total | 177 |
| Name | Category | Theorems |
|---|
add π | CompOp | 14 mathmath: exp_inr, inl_fst_add_inr_snd_eq, snd_add, mul_left_eq_one, inl_add, fst_add, DualNumber.exp_eps, exp_def, hasSum_expSeries_of_smul_comm, instContinuousAdd, inr_add, DualNumber.exp_smul_eps, mul_right_eq_one, exp_def_of_smul_comm
|
addCommGroup π | CompOp | β |
addCommMonoid π | CompOp | 20 mathmath: fstCLM_apply, lift_inlAlgHom_inrHom, hasSum_inr, lift_comp_inrHom, algHom_ext'_iff, map_comp_inrHom, sndCLM_apply, fst_sum, hasSum_inl, inrCLM_apply, inrHom_apply, hasSum_expSeries_of_smul_comm, snd_sum, inlCLM_apply, sndHom_comp_map, inl_sum, sndHom_apply, DualNumber.algHom_ext'_iff, liftEquiv_symm_apply_coe, inr_sum
|
addCommSemigroup π | CompOp | β |
addGroup π | CompOp | 1 mathmath: instIsUniformAddGroup
|
addGroupWithOne π | CompOp | 3 mathmath: fst_intCast, inl_intCast, snd_intCast
|
addMonoid π | CompOp | β |
addMonoidWithOne π | CompOp | 3 mathmath: inl_natCast, snd_natCast, fst_natCast
|
addSemigroup π | CompOp | β |
addZeroClass π | CompOp | β |
algebra' π | CompOp | 49 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, lift_inlAlgHom_inrHom, DualNumber.range_lift, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.imJ_fst_dualNumberEquiv, fstHom_comp_map, Quaternion.imI_fst_dualNumberEquiv, DualNumber.lift_apply_eps, lift_comp_inrHom, hasSum_snd_expSeries_of_smul_comm, fst_expSeries, algHom_ext'_iff, Quaternion.fst_imK_dualNumberEquiv_symm, algebraMap_eq_inl', DualNumber.lift_inlAlgHom_eps, DualNumber.lift_smul, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, lift_apply_inr, liftEquiv_apply, inlAlgHom_apply, Quaternion.fst_imJ_dualNumberEquiv_symm, Matrix.dualNumberEquiv_symm_apply, Quaternion.fst_imI_dualNumberEquiv_symm, DualNumber.lift_apply_apply, hasSum_expSeries_of_smul_comm, DualNumber.coe_lift_symm_apply, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, lift_def, DualNumber.range_inlAlgHom_sup_adjoin_eps, lift_comp_inlHom, liftEquivOfComm_symm_apply_coe, Matrix.dualNumberEquiv_apply, Quaternion.re_snd_dualNumberEquiv, lift_apply_inl, Quaternion.snd_imI_dualNumberEquiv_symm, DualNumber.lift_apply_inl, DualNumber.lift_op_smul, DualNumber.lift_comp_inlHom, DualNumber.algHom_ext'_iff, fstHom_apply, liftEquiv_symm_apply_coe, range_inlAlgHom_sup_adjoin_range_inr, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, snd_expSeries_of_smul_comm, range_liftAux, Quaternion.imK_snd_dualNumberEquiv
|
algebraBase π | CompOp | 1 mathmath: instIsScalarTower
|
commMonoid π | CompOp | β |
commRing π | CompOp | 16 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.imJ_fst_dualNumberEquiv, Quaternion.imI_fst_dualNumberEquiv, Quaternion.fst_imK_dualNumberEquiv_symm, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, Quaternion.fst_imJ_dualNumberEquiv_symm, Quaternion.fst_imI_dualNumberEquiv_symm, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, Quaternion.re_snd_dualNumberEquiv, Quaternion.snd_imI_dualNumberEquiv_symm, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, Quaternion.imK_snd_dualNumberEquiv
|
commSemiring π | CompOp | 2 mathmath: DualNumber.maximalIdeal_eq_span_singleton_eps, instIsScalarTower
|
distribMulAction π | CompOp | β |
fst π | CompOp | 63 mathmath: fstCLM_apply, snd_pow, snd_pow_eq_sum, nhds_def, isNilpotent_iff_isNilpotent_fst, hasSum_fst, fst_intCast, inl_fst_add_inr_snd_eq, Quaternion.imJ_fst_dualNumberEquiv, snd_list_prod, fst_exp, Quaternion.imI_fst_dualNumberEquiv, uniformContinuous_fst, fst_smul, fst_invOf, fst_expSeries, fst_inr, fst_comp_inr, Quaternion.fst_imK_dualNumberEquiv_symm, DualNumber.fst_eq_zero_iff_eps_dvd, eq_smul_exp_of_ne_zero, invertibleEquivInvertibleFst_symm_apply_invOf, fst_list_prod, norm_def, snd_exp, fst_add, Quaternion.imK_fst_dualNumberEquiv, fst_sum, Quaternion.re_fst_dualNumberEquiv, fst_one, invertibleEquivInvertibleFst_apply_invOf, snd_inv, Quaternion.fst_imJ_dualNumberEquiv_symm, Matrix.dualNumberEquiv_symm_apply, Quaternion.fst_imI_dualNumberEquiv_symm, exp_def, DualNumber.lift_apply_apply, snd_invOf, ext_iff, fst_neg, fst_inv, snd_mul, fst_pow, lift_def, nnnorm_def, DualNumber.fst_eps, fst_comp_inl, fst_map, Matrix.dualNumberEquiv_apply, fst_natCast, continuous_fst, fst_mul, fst_inl, isUnit_iff_isUnit_fst, fstHom_apply, DualNumber.snd_mul, fst_surjective, Quaternion.fst_re_dualNumberEquiv_symm, fst_sub, uniformity_def, eq_smul_exp_of_invertible, fst_zero, fst_mk
|
fstHom π | CompOp | 2 mathmath: fstHom_comp_map, fstHom_apply
|
inhabited π | CompOp | β |
inl π | CompOp | 47 mathmath: lift_inlAlgHom_inrHom, inv_inl, inl_fst_add_inr_snd_eq, inl_mul_inr, algebraMap_eq_inl', inl_injective, mul_left_eq_one, inl_add, inl_smul, inlHom_apply, hasSum_inl, isNilpotent_inl_iff, inl_neg, inl_mul, inlAlgHom_apply, inl_natCast, exp_def, inr_mul_inl, inl_mul_inl, nhds_inl, continuous_inl, hasSum_expSeries_of_smul_comm, inlCLM_apply, norm_inl, algebraMap_eq_inl, snd_inl, nnnorm_inl, IsEmbedding.inl, fst_comp_inl, lift_apply_inl, exp_inl, inl_sum, inl_zero, map_inl, DualNumber.lift_apply_inl, mul_right_eq_one, exp_def_of_smul_comm, uniformContinuous_inl, inl_mul_eq_smul, fst_inl, isUnit_inl_iff, inl_intCast, inl_pow, mul_inl_eq_op_smul, inl_sub, snd_comp_inl, inl_one
|
inlAlgHom π | CompOp | 12 mathmath: lift_inlAlgHom_inrHom, algHom_ext'_iff, map_comp_inlAlgHom, DualNumber.lift_inlAlgHom_eps, inlAlgHom_apply, DualNumber.coe_lift_symm_apply, DualNumber.range_inlAlgHom_sup_adjoin_eps, lift_comp_inlHom, DualNumber.lift_comp_inlHom, DualNumber.algHom_ext'_iff, liftEquiv_symm_apply_coe, range_inlAlgHom_sup_adjoin_range_inr
|
inlHom π | CompOp | 2 mathmath: inlHom_apply, algebraMap_eq_inlHom
|
inr π | CompOp | 42 mathmath: exp_inr, IsEmbedding.inr, lift_inlAlgHom_inrHom, TensorAlgebra.toTrivSqZeroExt_ΞΉ, hasSum_inr, inl_fst_add_inr_snd_eq, map_inr, snd_inr, fst_inr, fst_comp_inr, eq_smul_exp_of_ne_zero, inl_mul_inr, isNilpotent_inr, mul_left_eq_one, uniformContinuous_inr, inr_mul_inr, lift_apply_inr, inrCLM_apply, inrHom_apply, inr_neg, exp_def, inr_mul_inl, ExteriorAlgebra.toTrivSqZeroExt_ΞΉ, hasSum_expSeries_of_smul_comm, inr_sub, inr_smul, inr_injective, continuous_inr, snd_comp_inr, isUnit_inr_iff, inr_add, nnnorm_inr, nhds_inr, mul_right_eq_one, inr_zero, exp_def_of_smul_comm, DualNumber.inr_eq_smul_eps, range_inlAlgHom_sup_adjoin_range_inr, inr_sum, inv_inr, eq_smul_exp_of_invertible, norm_inr
|
inrHom π | CompOp | 7 mathmath: lift_inlAlgHom_inrHom, lift_comp_inrHom, algHom_ext'_iff, map_comp_inrHom, inrHom_apply, liftEquivOfComm_symm_apply_coe, liftEquiv_symm_apply_coe
|
instAlgebra π | CompOp | 38 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, TensorAlgebra.toTrivSqZeroExt_ΞΉ, CliffordAlgebraDualNumber.equiv_symm_eps, Quaternion.snd_re_dualNumberEquiv_symm, ExteriorAlgebra.toTrivSqZeroExt_comp_map, Quaternion.imJ_fst_dualNumberEquiv, fstHom_comp_map, map_inr, Quaternion.imI_fst_dualNumberEquiv, map_comp_inlAlgHom, Quaternion.fst_imK_dualNumberEquiv_symm, map_comp_inrHom, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, Quaternion.fst_imJ_dualNumberEquiv_symm, Matrix.dualNumberEquiv_symm_apply, Quaternion.fst_imI_dualNumberEquiv_symm, ExteriorAlgebra.toTrivSqZeroExt_ΞΉ, Quaternion.imJ_snd_dualNumberEquiv, liftEquivOfComm_apply, Quaternion.snd_imK_dualNumberEquiv_symm, sndHom_comp_map, map_comp_map, algebraMap_eq_inl, DualNumber.algHom_ext_iff, CliffordAlgebraDualNumber.equiv_ΞΉ, snd_map, fst_map, liftEquivOfComm_symm_apply_coe, Matrix.dualNumberEquiv_apply, Quaternion.re_snd_dualNumberEquiv, algebraMap_eq_inlHom, map_inl, Quaternion.snd_imI_dualNumberEquiv_symm, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, map_id, Quaternion.imK_snd_dualNumberEquiv
|
instInv π | CompOp | 14 mathmath: inv_inl, inv_one, DualNumber.inv_eps, mul_inv_cancel, inv_mul_cancel, invOf_eq_inv, snd_inv, inv_inv, isUnit_inv_iff, inv_neg, fst_inv, inv_zero, mul_inv_rev, inv_inr
|
instPowNatOfDistribMulActionMulOpposite π | CompOp | 13 mathmath: snd_pow, snd_pow_eq_sum, isNilpotent_iff_isNilpotent_fst, isNilpotent_inr, DualNumber.isNilpotent_iff_eps_dvd, isNilpotent_inl_iff, snd_pow_of_smul_comm, snd_pow_of_smul_comm', fst_pow, isUnit_or_isNilpotent_of_isMaximal_isNilpotent, isUnit_or_isNilpotent, inl_pow, DualNumber.isNilpotent_eps
|
invertibleEquivInvertibleFst π | CompOp | 2 mathmath: invertibleEquivInvertibleFst_symm_apply_invOf, invertibleEquivInvertibleFst_apply_invOf
|
invertibleFstOfInvertible π | CompOp | β |
invertibleOfInvertibleFst π | CompOp | β |
liftEquiv π | CompOp | 2 mathmath: liftEquiv_apply, liftEquiv_symm_apply_coe
|
liftEquivOfComm π | CompOp | 2 mathmath: liftEquivOfComm_apply, liftEquivOfComm_symm_apply_coe
|
map π | CompOp | 11 mathmath: ExteriorAlgebra.toTrivSqZeroExt_comp_map, fstHom_comp_map, map_inr, map_comp_inlAlgHom, map_comp_inrHom, sndHom_comp_map, map_comp_map, snd_map, fst_map, map_inl, map_id
|
monoid π | CompOp | 6 mathmath: isUnit_inv_iff, isUnit_inr_iff, isUnit_or_isNilpotent_of_isMaximal_isNilpotent, isUnit_inl_iff, isUnit_iff_isUnit_fst, isUnit_or_isNilpotent
|
mul π | CompOp | 28 mathmath: lift_inlAlgHom_inrHom, snd_list_prod, fst_invOf, invertibleEquivInvertibleFst_symm_apply_invOf, inl_mul_inr, fst_list_prod, mul_left_eq_one, inr_mul_inr, instContinuousMulOfContinuousSMulMulOppositeOfContinuousAdd, DualNumber.exists_mul_left_or_mul_right, invertibleEquivInvertibleFst_apply_invOf, mul_inv_cancel, inv_mul_cancel, invOf_eq_inv, inl_mul, inr_mul_inl, snd_invOf, inl_mul_inl, snd_mul, DualNumber.commute_eps_left, DualNumber.commute_eps_right, mul_right_eq_one, fst_mul, inl_mul_eq_smul, DualNumber.eps_mul_eps, DualNumber.snd_mul, mul_inv_rev, mul_inl_eq_op_smul
|
mulAction π | CompOp | β |
mulOneClass π | CompOp | β |
neg π | CompOp | 22 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, instContinuousNeg, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.imJ_fst_dualNumberEquiv, Quaternion.imI_fst_dualNumberEquiv, Quaternion.fst_imK_dualNumberEquiv_symm, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, inl_neg, Quaternion.fst_imJ_dualNumberEquiv_symm, Quaternion.fst_imI_dualNumberEquiv_symm, inr_neg, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, fst_neg, inv_neg, Quaternion.re_snd_dualNumberEquiv, Quaternion.snd_imI_dualNumberEquiv_symm, snd_neg, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, Quaternion.imK_snd_dualNumberEquiv
|
nonAssocRing π | CompOp | 1 mathmath: instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite
|
nonAssocSemiring π | CompOp | 2 mathmath: inlHom_apply, topologicalSemiring
|
one π | CompOp | 35 mathmath: exp_inr, Quaternion.snd_imJ_dualNumberEquiv_symm, inv_one, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.imJ_fst_dualNumberEquiv, snd_list_prod, instNormOneClass, Quaternion.imI_fst_dualNumberEquiv, fst_invOf, Quaternion.fst_imK_dualNumberEquiv_symm, invertibleEquivInvertibleFst_symm_apply_invOf, fst_list_prod, mul_left_eq_one, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, fst_one, invertibleEquivInvertibleFst_apply_invOf, mul_inv_cancel, inv_mul_cancel, invOf_eq_inv, Quaternion.fst_imJ_dualNumberEquiv_symm, DualNumber.exp_eps, Quaternion.fst_imI_dualNumberEquiv_symm, snd_invOf, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, Quaternion.re_snd_dualNumberEquiv, snd_one, DualNumber.exp_smul_eps, Quaternion.snd_imI_dualNumberEquiv_symm, mul_right_eq_one, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, inl_one, Quaternion.imK_snd_dualNumberEquiv
|
semiring π | CompOp | 69 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, lift_inlAlgHom_inrHom, TensorAlgebra.toTrivSqZeroExt_ΞΉ, DualNumber.range_lift, CliffordAlgebraDualNumber.equiv_symm_eps, Quaternion.snd_re_dualNumberEquiv_symm, ExteriorAlgebra.toTrivSqZeroExt_comp_map, Quaternion.imJ_fst_dualNumberEquiv, fstHom_comp_map, map_inr, Quaternion.imI_fst_dualNumberEquiv, DualNumber.lift_apply_eps, lift_comp_inrHom, algHom_ext'_iff, map_comp_inlAlgHom, Quaternion.fst_imK_dualNumberEquiv_symm, DualNumber.fst_eq_zero_iff_eps_dvd, algebraMap_eq_inl', DualNumber.lift_inlAlgHom_eps, DualNumber.isNilpotent_iff_eps_dvd, map_comp_inrHom, DualNumber.isMaximal_span_singleton_eps, DualNumber.lift_smul, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, lift_apply_inr, liftEquiv_apply, inlAlgHom_apply, Quaternion.fst_imJ_dualNumberEquiv_symm, Matrix.dualNumberEquiv_symm_apply, Quaternion.fst_imI_dualNumberEquiv_symm, DualNumber.lift_apply_apply, ExteriorAlgebra.toTrivSqZeroExt_ΞΉ, DualNumber.coe_lift_symm_apply, Quaternion.imJ_snd_dualNumberEquiv, liftEquivOfComm_apply, Quaternion.snd_imK_dualNumberEquiv_symm, sndHom_comp_map, map_comp_map, lift_def, algebraMap_eq_inl, DualNumber.range_inlAlgHom_sup_adjoin_eps, DualNumber.algHom_ext_iff, CliffordAlgebraDualNumber.equiv_ΞΉ, snd_map, DualNumber.instIsLocalRing, fst_map, lift_comp_inlHom, liftEquivOfComm_symm_apply_coe, Matrix.dualNumberEquiv_apply, Quaternion.re_snd_dualNumberEquiv, algebraMap_eq_inlHom, lift_apply_inl, map_inl, Quaternion.snd_imI_dualNumberEquiv_symm, DualNumber.lift_apply_inl, DualNumber.lift_op_smul, DualNumber.lift_comp_inlHom, DualNumber.algHom_ext'_iff, DualNumber.ideal_trichotomy, fstHom_apply, liftEquiv_symm_apply_coe, DualNumber.instIsPrincipalIdealRing, range_inlAlgHom_sup_adjoin_range_inr, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, map_id, range_liftAux, Quaternion.imK_snd_dualNumberEquiv
|
smul π | CompOp | 20 mathmath: isScalarTower, fst_smul, eq_smul_exp_of_ne_zero, DualNumber.lift_smul, inl_smul, snd_smul, smulCommClass, isCentralScalar, inr_smul, instL1IsBoundedSMul, instContinuousSMul, CliffordAlgebraDualNumber.equiv_ΞΉ, DualNumber.exp_smul_eps, DualNumber.lift_op_smul, inl_mul_eq_smul, DualNumber.inr_eq_smul_eps, instIsScalarTower, mul_inl_eq_op_smul, eq_smul_exp_of_invertible, instContinuousConstSMul
|
snd π | CompOp | 54 mathmath: snd_pow, Quaternion.snd_imJ_dualNumberEquiv_symm, snd_pow_eq_sum, nhds_def, inl_fst_add_inr_snd_eq, Quaternion.snd_re_dualNumberEquiv_symm, snd_list_prod, continuous_snd, snd_add, snd_inr, snd_surjective, snd_mk, eq_smul_exp_of_ne_zero, invertibleEquivInvertibleFst_symm_apply_invOf, uniformContinuous_snd, norm_def, mul_left_eq_one, snd_exp, sndCLM_apply, snd_inv, snd_smul, Matrix.dualNumberEquiv_symm_apply, exp_def, hasSum_snd, DualNumber.lift_apply_apply, snd_invOf, snd_sum, ext_iff, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, snd_mul, lift_def, nnnorm_def, snd_inl, snd_comp_inr, DualNumber.snd_eps, snd_map, snd_natCast, Matrix.dualNumberEquiv_apply, Quaternion.re_snd_dualNumberEquiv, sndHom_apply, snd_one, Quaternion.snd_imI_dualNumberEquiv_symm, mul_right_eq_one, snd_neg, snd_sub, DualNumber.snd_mul, snd_zero, Quaternion.imI_snd_dualNumberEquiv, snd_comp_inl, uniformity_def, eq_smul_exp_of_invertible, snd_intCast, Quaternion.imK_snd_dualNumberEquiv
|
sndHom π | CompOp | 2 mathmath: sndHom_comp_map, sndHom_apply
|
sub π | CompOp | 4 mathmath: inr_sub, snd_sub, fst_sub, inl_sub
|
zero π | CompOp | 33 mathmath: Quaternion.snd_imJ_dualNumberEquiv_symm, isNilpotent_iff_isNilpotent_fst, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.imJ_fst_dualNumberEquiv, Quaternion.imI_fst_dualNumberEquiv, DualNumber.inv_eps, Quaternion.fst_imK_dualNumberEquiv_symm, isNilpotent_inr, DualNumber.isNilpotent_iff_eps_dvd, Quaternion.imK_fst_dualNumberEquiv, Quaternion.re_fst_dualNumberEquiv, inr_mul_inr, isNilpotent_inl_iff, Quaternion.fst_imJ_dualNumberEquiv_symm, Quaternion.fst_imI_dualNumberEquiv_symm, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.snd_imK_dualNumberEquiv_symm, instL1IsBoundedSMul, isUnit_or_isNilpotent_of_isMaximal_isNilpotent, Quaternion.re_snd_dualNumberEquiv, inl_zero, Quaternion.snd_imI_dualNumberEquiv_symm, inr_zero, inv_zero, DualNumber.eps_mul_eps, isUnit_or_isNilpotent, snd_zero, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.imI_snd_dualNumberEquiv, inv_inr, DualNumber.isNilpotent_eps, fst_zero, Quaternion.imK_snd_dualNumberEquiv
|