DualNumber

📁 Source: Mathlib/Algebra/DualNumber.lean

Statistics

Metric	Count
Definitions eps, instRepr, termε, «term_[ε]»	4
Theorems algHom_ext, algHom_ext', algHom_ext'_iff, algHom_ext_iff, coe_lift_symm_apply, commute_eps_left, commute_eps_right, eps_mul_eps, eps_pow_two, fst_eps, inr_eq_smul_eps, inv_eps, lift_apply_apply, lift_apply_eps, lift_apply_inl, lift_comp_inlHom, lift_inlAlgHom_eps, lift_op_smul, lift_smul, range_inlAlgHom_sup_adjoin_eps, range_lift, ringHom_ext, ringHom_ext_iff, snd_eps, snd_mul	25
Total	29

DualNumber

Definitions

Name	Category	Theorems
eps 📖	CompOp	25 math math: CliffordAlgebraDualNumber.equiv_symm_eps, lift_apply_eps, inv_eps, fst_eq_zero_iff_eps_dvd, maximalIdeal_eq_span_singleton_eps, lift_inlAlgHom_eps, isNilpotent_iff_eps_dvd, isMaximal_span_singleton_eps, exp_eps, ringHom_ext_iff, coe_lift_symm_apply, range_inlAlgHom_sup_adjoin_eps, fst_eps, commute_eps_left, algHom_ext_iff, snd_eps, CliffordAlgebraDualNumber.equiv_ι, commute_eps_right, eps_pow_two, exp_smul_eps, algHom_ext'_iff, ideal_trichotomy, inr_eq_smul_eps, eps_mul_eps, isNilpotent_eps
instRepr 📖	CompOp	—
termε 📖	CompOp	—
«term_[ε]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.right Algebra.id TrivSqZeroExt.instAlgebra CommSemigroup.isCentralScalar NonUnitalCommSemiring.toCommSemigroup CommSemiring.toNonUnitalCommSemiring AlgHom.funLike eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	SMulCommClass.opposite_mid IsScalarTower.right CommSemigroup.isCentralScalar algHom_ext' Algebra.ext_id IsScalarTower.left IsScalarTower.opposite_mid Algebra.to_smulCommClass LinearMap.ext_ring RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul' TrivSqZeroExt.isScalarTower one_smul
algHom_ext' 📖	—	AlgHom.comp DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass TrivSqZeroExt.inlAlgHom LinearMap.comp RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap LinearMap.restrictScalars TrivSqZeroExt.addCommMonoid TrivSqZeroExt.module LinearMap.IsScalarTower.compatibleSMul' TrivSqZeroExt.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction LinearMap.toSpanSingleton eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul' TrivSqZeroExt.isScalarTower TrivSqZeroExt.algHom_ext' LinearMap.ext LinearMap.IsScalarTower.compatibleSMul inr_eq_smul_eps DFunLike.congr_fun
algHom_ext'_iff 📖	mathematical	—	AlgHom.comp DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass TrivSqZeroExt.inlAlgHom LinearMap.comp RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap LinearMap.restrictScalars TrivSqZeroExt.addCommMonoid TrivSqZeroExt.module LinearMap.IsScalarTower.compatibleSMul' TrivSqZeroExt.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction LinearMap.toSpanSingleton eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul' TrivSqZeroExt.isScalarTower algHom_ext'
algHom_ext_iff 📖	mathematical	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.right Algebra.id TrivSqZeroExt.instAlgebra CommSemigroup.isCentralScalar NonUnitalCommSemiring.toCommSemigroup CommSemiring.toNonUnitalCommSemiring AlgHom.funLike eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	SMulCommClass.opposite_mid IsScalarTower.right CommSemigroup.isCentralScalar algHom_ext
coe_lift_symm_apply 📖	mathematical	—	AlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DFunLike.coe Equiv DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift AlgHom.comp TrivSqZeroExt.inlAlgHom AlgHom.funLike eps AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass
commute_eps_left 📖	mathematical	—	Commute DualNumber TrivSqZeroExt.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul MulOpposite DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toOppositeModule eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne	—	TrivSqZeroExt.ext MulZeroClass.zero_mul MulZeroClass.mul_zero one_mul zero_add mul_one zero_smul add_zero
commute_eps_right 📖	mathematical	—	Commute DualNumber TrivSqZeroExt.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul MulOpposite DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toOppositeModule eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne	—	Commute.symm commute_eps_left
eps_mul_eps 📖	mathematical	—	DualNumber TrivSqZeroExt.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul MulOpposite DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toOppositeModule eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne TrivSqZeroExt.zero	—	TrivSqZeroExt.inr_mul_inr
eps_pow_two 📖	mathematical	—	DualNumber Monoid.toPow TrivSqZeroExt.monoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MulOpposite MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne TrivSqZeroExt.zero	—	SMulCommClass.opposite_mid IsScalarTower.left pow_two eps_mul_eps
fst_eps 📖	mathematical	—	TrivSqZeroExt.fst eps	—	—
inr_eq_smul_eps 📖	mathematical	—	TrivSqZeroExt.inr MulZeroClass.toZero MulZeroOneClass.toMulZeroClass DualNumber TrivSqZeroExt.smul SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero eps MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	TrivSqZeroExt.ext MulZeroClass.mul_zero mul_one
inv_eps 📖	mathematical	—	DualNumber TrivSqZeroExt.instInv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring SMulZeroClass.toSMul MulOpposite AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toOppositeModule instDistribSMul eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne TrivSqZeroExt.zero	—	TrivSqZeroExt.inv_inr
lift_apply_apply 📖	mathematical	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass AlgHom.funLike Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift Distrib.toAdd TrivSqZeroExt.fst TrivSqZeroExt.snd	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass
lift_apply_eps 📖	mathematical	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass AlgHom.funLike Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift eps AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass one_mul zero_add
lift_apply_inl 📖	mathematical	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass AlgHom.funLike Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift TrivSqZeroExt.inl	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass lift_apply_apply TrivSqZeroExt.fst_inl TrivSqZeroExt.snd_inl map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.zero_mul add_zero
lift_comp_inlHom 📖	mathematical	—	AlgHom.comp DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass DFunLike.coe Equiv AlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift TrivSqZeroExt.inlAlgHom	—	AlgHom.ext SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass lift_apply_inl
lift_inlAlgHom_eps 📖	mathematical	—	DFunLike.coe Equiv AlgHom TrivSqZeroExt TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DualNumber EquivLike.toFunLike Equiv.instEquivLike lift TrivSqZeroExt.inlAlgHom eps AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne eps_mul_eps commute_eps_left AlgHom.funLike AlgHom.id	—	Equiv.apply_symm_apply SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass
lift_op_smul 📖	mathematical	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass AlgHom.funLike Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift MulOpposite TrivSqZeroExt.smul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulOpposite.instMonoid MulOpposite.instSemiring MulOpposite.op	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass TrivSqZeroExt.mul_inl_eq_op_smul map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass lift_apply_inl
lift_smul 📖	mathematical	—	DFunLike.coe AlgHom DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass AlgHom.funLike Equiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift TrivSqZeroExt.smul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass TrivSqZeroExt.inl_mul_eq_smul map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass lift_apply_inl
range_inlAlgHom_sup_adjoin_eps 📖	mathematical	—	Subalgebra TrivSqZeroExt TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra AlgHom.range TrivSqZeroExt.inlAlgHom Algebra.adjoin DualNumber Set Set.instSingletonSet eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass TrivSqZeroExt.inl_fst_add_inr_snd_eq inr_eq_smul_eps TrivSqZeroExt.inl_mul_eq_smul AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass le_sup_left Set.mem_range_self MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass le_sup_right Algebra.subset_adjoin Set.mem_singleton
range_lift 📖	mathematical	—	AlgHom.range DualNumber TrivSqZeroExt.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction TrivSqZeroExt.algebra' Algebra.toModule IsScalarTower.right IsScalarTower.opposite_mid CommSemiring.toSemiring Algebra.to_smulCommClass DFunLike.coe Equiv AlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike lift Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Algebra.adjoin Set Set.instSingletonSet	—	SMulCommClass.opposite_mid IsScalarTower.left IsScalarTower.right IsScalarTower.opposite_mid Algebra.to_smulCommClass Algebra.map_sup AlgHom.map_adjoin Set.image_singleton lift_apply_eps lift_comp_inlHom Algebra.map_top
ringHom_ext 📖	—	RingHom.comp DualNumber Semiring.toNonAssocSemiring CommSemiring.toSemiring TrivSqZeroExt.nonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Semiring.toOppositeModule algebraMap TrivSqZeroExt.semiring SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.right Algebra.id TrivSqZeroExt.instAlgebra CommSemigroup.isCentralScalar NonUnitalCommSemiring.toCommSemigroup CommSemiring.toNonUnitalCommSemiring DFunLike.coe RingHom RingHom.instFunLike eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	SMulCommClass.opposite_mid IsScalarTower.right CommSemigroup.isCentralScalar DFunLike.congr_fun algHom_ext
ringHom_ext_iff 📖	mathematical	—	RingHom.comp DualNumber Semiring.toNonAssocSemiring CommSemiring.toSemiring TrivSqZeroExt.nonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Semiring.toOppositeModule algebraMap TrivSqZeroExt.semiring SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.right Algebra.id TrivSqZeroExt.instAlgebra CommSemigroup.isCentralScalar NonUnitalCommSemiring.toCommSemigroup CommSemiring.toNonUnitalCommSemiring DFunLike.coe RingHom RingHom.instFunLike eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	SMulCommClass.opposite_mid IsScalarTower.right CommSemigroup.isCentralScalar ringHom_ext
snd_eps 📖	mathematical	—	TrivSqZeroExt.snd eps	—	—
snd_mul 📖	mathematical	—	TrivSqZeroExt.snd DualNumber TrivSqZeroExt.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul MulOpposite DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toOppositeModule TrivSqZeroExt.fst	—	—

---

← Back to Index