NonUnitalHom

📁 Source: Mathlib/Algebra/Algebra/NonUnitalHom.lean

Statistics

Metric	Count
Definitions hasCoe, toNonUnitalAlgHom, NonUnitalAlgHom, apply, comp, fst, id, inl, inr, instFunLike, instFunLike_1, instInhabited, instOneId, instZero, inverse, inverse', prod, prodEquiv, restrictScalars, snd, toDistribMulActionHom, toMulHom, NonUnitalAlgHomClass, instCoeTCNonUnitalAlgHomId, instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass, toNonUnitalAlgHom, toNonUnitalAlgSemiHom, NonUnitalAlgSemiHomClass, «term_→ₙₐ[_]_», «term_→ₙₐ_», «term_→ₛₙₐ[_]_»	31
Theorems instNonUnitalAlgHomClassOfAlgHomClass, toNonUnitalAlgHom_eq_coe, addHomMk_coe, coe_coe, coe_comp, coe_distribMulActionHom_mk, coe_id, coe_injective, coe_inl, coe_inr, coe_inverse, coe_inverse', coe_mk, coe_mulHom_mk, coe_one, coe_prod, coe_restrictScalars, coe_restrictScalars', coe_to_distribMulActionHom, coe_to_mulHom, coe_zero, comp_apply, congr_fun, ext, ext_iff, fst_apply, fst_prod, fst_toFun, inl_apply, inr_apply, instNonUnitalAlgSemiHomClass, map_add, map_mul, map_mul', map_smul, map_zero, mk_coe, one_apply, prodEquiv_apply, prodEquiv_symm_apply, prod_apply, prod_fst_snd, prod_toFun, restrictScalars_apply, restrictScalars_injective, snd_apply, snd_prod, snd_toFun, toDistribMulActionHom_eq_coe, toFun_eq_coe, toMulHom_eq_coe, to_distribMulActionHom_injective, to_mulHom_injective, zero_apply, instLinearMapClass, instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom, toNonUnitalRingHomClass, toDistribMulActionSemiHomClass, toMulHomClass	59
Total	90

AlgHom

Definitions

Name	Category	Theorems
toNonUnitalAlgHom 📖	CompOp	2 math math: Unitization.algHom_ext'_iff, toNonUnitalAlgHom_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonUnitalAlgHomClassOfAlgHomClass 📖	mathematical	—	NonUnitalAlgHomClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule	—	map_smul SemilinearMapClass.toMulActionSemiHomClass AlgHomClass.linearMapClass RingHomClass.toAddMonoidHomClass AlgHomClass.toRingHomClass MonoidHomClass.toMulHomClass RingHomClass.toMonoidHomClass
toNonUnitalAlgHom_eq_coe 📖	mathematical	—	toNonUnitalAlgHom NonUnitalAlgHomClass.toNonUnitalAlgHom AlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule funLike instNonUnitalAlgHomClassOfAlgHomClass algHomClass	—	—

AlgHom.NonUnitalAlgHom

Definitions

Name	Category	Theorems
hasCoe 📖	CompOp	—

NonUnitalAlgHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	12 math math: range_comp_le_range, Unitization.algHom_ext'_iff, NonUnitalSubalgebra.iSupLift_comp_inclusion, prodEquiv_symm_apply, coe_comp, snd_prod, Unitization.lift_symm_apply, fst_prod, range_comp, NonUnitalSubalgebra.map_map, comp_apply, subtype_comp_codRestrict
fst 📖	CompOp	5 math math: fst_toFun, prod_fst_snd, prodEquiv_symm_apply, fst_prod, fst_apply
id 📖	CompOp	5 math math: NonUnitalSubalgebra.inclusion_self, NonUnitalAlgebra.range_id, coe_id, NonUnitalSubalgebra.map_id, NonUnitalStarSubalgebra.inclusion_self
inl 📖	CompOp	2 math math: inl_apply, coe_inl
inr 📖	CompOp	2 math math: coe_inr, inr_apply
instFunLike 📖	CompOp	17 math math: MonoidAlgebra.liftMagma_apply_apply, Unitization.inrNonUnitalAlgHom_toFun, fst_toFun, AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply, prod_apply, coe_coe, LieHom.toNonUnitalAlgHom_toFun, AddMonoidAlgebra.liftMagma_apply_apply, toFun_eq_coe, LieHom.toNonUnitalAlgHom_apply, snd_apply, MonoidAlgebra.mapDomainNonUnitalAlgHom_apply, prod_toFun, Unitization.inrNonUnitalAlgHom_apply, coe_injective, fst_apply, snd_toFun
instFunLike_1 📖	CompOp	87 math math: map_smul, congr_fun, mk_coe, one_apply, NonUnitalSubalgebraClass.coe_subtype, range_comp_le_range, coe_lmul_eq_mul, NonUnitalSubalgebra.inclusion_mk, NonUnitalSubalgebra.topologicalClosure_map_le, NonUnitalSubalgebra.inclusion_right, FreeNonUnitalNonAssocAlgebra.of_comp_lift, NonUnitalSubalgebra.topologicalClosure_map, toDistribMulActionHom_eq_coe, CStarMatrix.norm_def', FreeNonUnitalNonAssocAlgebra.lift_unique, NonUnitalSubalgebra.iSupLift_of_mem, prod_apply, zero_apply, Unitization.lift_symm_apply_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, FreeLieAlgebra.liftAux_map_smul, NonUnitalAlgebra.range_id, map_mul, coe_distribMulActionHom_mk, coe_restrictScalars, restrictScalars_apply, NonUnitalSubalgebra.inclusion_injective, NonUnitalSubalgebra.iSupLift_mk, map_zero, injective_codRestrict, coe_inr, coe_Lmul, coe_one, NonUnitalSubalgebra.toSubring_subtype, FreeLieAlgebra.liftAux_map_add, coe_comp, FreeNonUnitalNonAssocAlgebra.lift_symm_apply, NonUnitalSubalgebra.iSupLift_inclusion, WeakDual.CharacterSpace.coe_toNonUnitalAlgHom, coe_prod, coe_restrictScalars', NonUnitalSubalgebraClass.subtype_injective, FreeLieAlgebra.liftAux_map_mul, NonUnitalSubalgebra.inclusion_inclusion, NonUnitalStarAlgHom.coe_toNonUnitalAlgHom, inl_apply, ext_iff, Unitization.lift_range, coe_mulHom_mk, FreeLieAlgebra.liftAux_spec, addHomMk_coe, map_add, coe_inverse, NonUnitalSubalgebra.map_topologicalClosure_le, LinearMap.nonUnitalAlgHom_comp_convMul_distrib, comp_mul', coe_inl, prod_toFun, NonUnitalAlgebra.map_top, toAlgHom_apply, toMulHom_eq_coe, coe_id, coe_inverse', NonUnitalAlgebra.comap_top, range_comp, Unitization.lift_range_le, NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype, NonUnitalAlgebra.map_bot, coe_mk, NonUnitalStarAlgHom.coe_mk', inr_apply, NonUnitalSubalgebra.coe_inclusion, NonUnitalSubalgebraClass.subtype_apply, NonUnitalAlgebra.range_eq_top, coe_zero, instNonUnitalAlgSemiHomClass, Unitization.lift_apply_apply, coe_to_mulHom, NonUnitalSubalgebra.map_map, FreeNonUnitalNonAssocAlgebra.lift_of_apply, comp_apply, coe_codRestrict, FreeNonUnitalNonAssocAlgebra.hom_ext_iff, NonUnitalSubalgebra.map_id, NonUnitalSubalgebra.range_val, FreeNonUnitalNonAssocAlgebra.lift_comp_of, coe_to_distribMulActionHom
instInhabited 📖	CompOp	—
instOneId 📖	CompOp	3 math math: one_apply, prod_fst_snd, coe_one
instZero 📖	CompOp	3 math math: zero_apply, toAlgHom_zero, coe_zero
inverse 📖	CompOp	1 math math: coe_inverse
inverse' 📖	CompOp	1 math math: coe_inverse'
prod 📖	CompOp	7 math math: prod_apply, prod_fst_snd, prodEquiv_apply, coe_prod, snd_prod, fst_prod, prod_toFun
prodEquiv 📖	CompOp	2 math math: prodEquiv_apply, prodEquiv_symm_apply
restrictScalars 📖	CompOp	4 math math: restrictScalars_injective, coe_restrictScalars, restrictScalars_apply, coe_restrictScalars'
snd 📖	CompOp	5 math math: prod_fst_snd, prodEquiv_symm_apply, snd_prod, snd_apply, snd_toFun
toDistribMulActionHom 📖	CompOp	7 math math: toDistribMulActionHom_eq_coe, WeakDual.CharacterSpace.toAlgHom_apply, PositiveLinearMap.gnsStarAlgHom_apply, toFun_eq_coe, map_mul', Pi.evalStarAlgHom_apply, NonUnitalStarAlgHom.map_star'
toMulHom 📖	CompOp	6 math math: SkewMonoidAlgebra.nonUnitalAlgHom_ext'_iff, MonoidAlgebra.nonUnitalAlgHom_ext'_iff, AddMonoidAlgebra.nonUnitalAlgHom_ext'_iff, MonoidAlgebra.liftMagma_symm_apply, AddMonoidAlgebra.liftMagma_symm_apply, toMulHom_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addHomMk_coe 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe NonUnitalAlgHom instFunLike_1 map_add AddMonoidHomClass.toAddHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass AddHomClass.toAddHom	—	map_add AddMonoidHomClass.toAddHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass
coe_coe 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike NonUnitalAlgHomClass.toNonUnitalAlgSemiHom	—	—
coe_comp 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 comp	—	—
coe_distribMulActionHom_mk 📖	mathematical	DFunLike.coe NonUnitalAlgHom instFunLike_1 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike MulActionHom.toFun AddZero.toAdd DistribMulActionHom.toMulActionHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	DistribMulActionSemiHomClass.toDistribMulActionHom NonUnitalAlgHom instFunLike_1 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass
coe_id 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 id	—	—
coe_injective 📖	mathematical	—	NonUnitalAlgHom DFunLike.coe instFunLike	—	—
coe_inl 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 inl MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
coe_inr 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
coe_inverse 📖	mathematical	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 inverse	—	—
coe_inverse' 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike NonUnitalAlgHom instFunLike_1	DFunLike.coe NonUnitalAlgHom instFunLike_1 inverse'	—	—
coe_mk 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike MulActionHom.toFun AddZero.toAdd DistribMulActionHom.toMulActionHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	DFunLike.coe NonUnitalAlgHom instFunLike_1 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
coe_mulHom_mk 📖	mathematical	DFunLike.coe NonUnitalAlgHom instFunLike_1 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike MulActionHom.toFun AddZero.toAdd DistribMulActionHom.toMulActionHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	MulHomClass.toMulHom NonUnitalAlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instFunLike_1 NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass
coe_one 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 instOneId	—	—
coe_prod 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 prod Pi.prod	—	—
coe_restrictScalars 📖	mathematical	—	NonUnitalRingHomClass.toNonUnitalRingHom NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgSemiHomClass restrictScalars	—	NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgSemiHomClass
coe_restrictScalars' 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 restrictScalars	—	—
coe_to_distribMulActionHom 📖	mathematical	—	DFunLike.coe DistribMulActionHom AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribMulAction.instFunLike DistribMulActionSemiHomClass.toDistribMulActionHom NonUnitalAlgHom instFunLike_1 NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass	—	NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass
coe_to_mulHom 📖	mathematical	—	DFunLike.coe MulHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib MulHom.funLike MulHomClass.toMulHom NonUnitalAlgHom instFunLike_1 NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass	—	NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass
coe_zero 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 instZero Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
comp_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 comp	—	—
congr_fun 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1	—	—
ext 📖	—	DFunLike.coe NonUnitalAlgHom instFunLike_1	—	—	coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1	—	ext
fst_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike fst	—	—
fst_prod 📖	mathematical	—	comp MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid fst prod MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId
fst_toFun 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike fst	—	—
inl_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 inl MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
inr_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike_1 inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
instNonUnitalAlgSemiHomClass 📖	mathematical	—	NonUnitalAlgSemiHomClass NonUnitalAlgHom instFunLike_1	—	MulActionHom.map_smul' DistribMulActionHom.map_add' DistribMulActionHom.map_zero' map_mul'
map_add 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	map_add AddMonoidHomClass.toAddHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass
map_mul 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	map_mul NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass
map_mul' 📖	mathematical	—	MulActionHom.toFun DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DistribMulActionHom.toMulActionHom toDistribMulActionHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
map_smul 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	MulActionSemiHomClass.map_smulₛₗ DistribMulActionSemiHomClass.toMulActionSemiHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass
map_zero 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass
mk_coe 📖	mathematical	DFunLike.coe NonUnitalAlgHom instFunLike_1 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike MulActionHom.toFun AddZero.toAdd DistribMulActionHom.toMulActionHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NonUnitalAlgHom instFunLike_1	—	—
one_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 instOneId	—	—
prodEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike prodEquiv prod	—	—
prodEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm prodEquiv comp fst snd	—	—
prod_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike prod Pi.prod instFunLike_1	—	—
prod_fst_snd 📖	mathematical	—	prod Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid fst snd NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instOneId	—	coe_injective Pi.prod_fst_snd
prod_toFun 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike prod Pi.prod instFunLike_1	—	—
restrictScalars_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass instFunLike_1 restrictScalars	—	—
restrictScalars_injective 📖	mathematical	—	NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass restrictScalars	—	ext congr_fun
snd_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike snd	—	—
snd_prod 📖	mathematical	—	comp MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid snd prod MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId
snd_toFun 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Prod.instNonUnitalNonAssocSemiring Prod.distribMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instFunLike snd	—	—
toDistribMulActionHom_eq_coe 📖	mathematical	—	toDistribMulActionHom DistribMulActionSemiHomClass.toDistribMulActionHom NonUnitalAlgHom instFunLike_1 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass	—	—
toFun_eq_coe 📖	mathematical	—	MulActionHom.toFun DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DistribMulActionHom.toMulActionHom toDistribMulActionHom NonUnitalAlgHom instFunLike	—	—
toMulHom_eq_coe 📖	mathematical	—	toMulHom MulHomClass.toMulHom NonUnitalAlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instFunLike_1 NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass	—	—
to_distribMulActionHom_injective 📖	—	DistribMulActionSemiHomClass.toDistribMulActionHom NonUnitalAlgHom instFunLike_1 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass	—	—	NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass ext DistribMulActionHom.congr_fun
to_mulHom_injective 📖	—	MulHomClass.toMulHom NonUnitalAlgHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instFunLike_1 NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass	—	—	NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass ext DFunLike.congr_fun
zero_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom instFunLike_1 instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—

NonUnitalAlgHom.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

NonUnitalAlgHomClass

Definitions

Name	Category	Theorems
instCoeTCNonUnitalAlgHomId 📖	CompOp	—
instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass 📖	CompOp	—
toNonUnitalAlgHom 📖	CompOp	5 math math: AlgHom.toNonUnitalAlgHom_eq_coe, NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype, Unitization.lift_symm_apply, NonUnitalStarSubalgebra.inclusion_self, NonUnitalAlgHom.subtype_comp_codRestrict
toNonUnitalAlgSemiHom 📖	CompOp	1 math math: NonUnitalAlgHom.coe_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLinearMapClass 📖	mathematical	—	LinearMapClass NonUnitalNonAssocSemiring.toAddCommMonoid	—	AddMonoidHomClass.toAddHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass DistribMulActionSemiHomClass.toMulActionSemiHomClass
instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom 📖	mathematical	—	SemilinearMapClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AddMonoidHomClass.toAddHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass DistribMulActionSemiHomClass.toMulActionSemiHomClass
toNonUnitalRingHomClass 📖	mathematical	—	NonUnitalRingHomClass	—	NonUnitalAlgSemiHomClass.toMulHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass

NonUnitalAlgSemiHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toDistribMulActionSemiHomClass 📖	mathematical	—	DistribMulActionSemiHomClass DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	—
toMulHomClass 📖	mathematical	—	MulHomClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—

(root)

Definitions

Name	Category	Theorems
NonUnitalAlgHom 📖	CompData	113 math math: NonUnitalAlgHom.map_smul, NonUnitalAlgHom.congr_fun, MonoidAlgebra.liftMagma_apply_apply, NonUnitalAlgHom.mk_coe, NonUnitalAlgHom.one_apply, Unitization.inrNonUnitalAlgHom_toFun, NonUnitalSubalgebraClass.coe_subtype, NonUnitalAlgHom.fst_toFun, NonUnitalAlgHom.range_comp_le_range, NonUnitalAlgHom.restrictScalars_injective, AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply, NonUnitalAlgHom.coe_lmul_eq_mul, NonUnitalSubalgebra.inclusion_mk, NonUnitalSubalgebra.topologicalClosure_map_le, NonUnitalSubalgebra.inclusion_right, FreeNonUnitalNonAssocAlgebra.of_comp_lift, NonUnitalSubalgebra.topologicalClosure_map, NonUnitalAlgHom.toDistribMulActionHom_eq_coe, CStarMatrix.norm_def', FreeNonUnitalNonAssocAlgebra.lift_unique, NonUnitalSubalgebra.iSupLift_of_mem, NonUnitalAlgHom.prod_apply, NonUnitalAlgHom.zero_apply, Unitization.lift_symm_apply_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, FreeLieAlgebra.liftAux_map_smul, NonUnitalAlgebra.range_id, NonUnitalAlgHom.map_mul, NonUnitalAlgHom.subsingleton, NonUnitalAlgHom.coe_distribMulActionHom_mk, NonUnitalAlgHom.coe_restrictScalars, NonUnitalAlgHom.restrictScalars_apply, NonUnitalAlgHom.toAlgHom_zero, NonUnitalAlgHom.prod_fst_snd, NonUnitalSubalgebra.inclusion_injective, NonUnitalAlgHom.prodEquiv_apply, NonUnitalSubalgebra.iSupLift_mk, NonUnitalAlgHom.prodEquiv_symm_apply, NonUnitalAlgHom.coe_coe, NonUnitalAlgHom.map_zero, NonUnitalAlgHom.injective_codRestrict, NonUnitalAlgHom.coe_inr, NonUnitalAlgHom.coe_Lmul, NonUnitalAlgHom.coe_one, NonUnitalSubalgebra.toSubring_subtype, FreeLieAlgebra.liftAux_map_add, NonUnitalAlgHom.coe_comp, FreeNonUnitalNonAssocAlgebra.lift_symm_apply, NonUnitalSubalgebra.iSupLift_inclusion, WeakDual.CharacterSpace.coe_toNonUnitalAlgHom, NonUnitalAlgHom.coe_prod, NonUnitalAlgHom.coe_restrictScalars', NonUnitalSubalgebraClass.subtype_injective, LieHom.toNonUnitalAlgHom_toFun, FreeLieAlgebra.liftAux_map_mul, NonUnitalSubalgebra.inclusion_inclusion, NonUnitalStarAlgHom.coe_toNonUnitalAlgHom, NonUnitalAlgHom.inl_apply, NonUnitalAlgHom.ext_iff, Unitization.lift_range, NonUnitalAlgHom.coe_mulHom_mk, FreeLieAlgebra.liftAux_spec, NonUnitalAlgHom.addHomMk_coe, Unitization.lift_symm_apply, NonUnitalAlgHom.map_add, AddMonoidAlgebra.liftMagma_apply_apply, NonUnitalAlgHom.toFun_eq_coe, NonUnitalAlgHom.coe_inverse, MonoidAlgebra.liftMagma_symm_apply, AddMonoidAlgebra.liftMagma_symm_apply, NonUnitalSubalgebra.map_topologicalClosure_le, LieHom.toNonUnitalAlgHom_apply, LinearMap.nonUnitalAlgHom_comp_convMul_distrib, NonUnitalAlgHom.comp_mul', NonUnitalAlgHom.snd_apply, NonUnitalAlgHom.coe_inl, MonoidAlgebra.mapDomainNonUnitalAlgHom_apply, NonUnitalAlgHom.prod_toFun, NonUnitalAlgebra.map_top, NonUnitalAlgHom.toAlgHom_apply, NonUnitalAlgHom.toMulHom_eq_coe, NonUnitalAlgHom.coe_id, NonUnitalAlgHom.coe_inverse', Unitization.inrNonUnitalAlgHom_apply, NonUnitalAlgebra.comap_top, NonUnitalAlgHom.range_comp, Unitization.lift_range_le, NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype, NonUnitalAlgHom.coe_injective, NonUnitalAlgebra.map_bot, NonUnitalAlgHom.coe_mk, NonUnitalStarAlgHom.coe_mk', NonUnitalAlgHom.inr_apply, NonUnitalSubalgebra.coe_inclusion, NonUnitalSubalgebraClass.subtype_apply, NonUnitalAlgebra.range_eq_top, NonUnitalAlgHom.coe_zero, NonUnitalAlgHom.instNonUnitalAlgSemiHomClass, Unitization.lift_apply_apply, NonUnitalAlgHom.coe_to_mulHom, NonUnitalSubalgebra.map_map, NonUnitalAlgHom.fst_apply, FreeNonUnitalNonAssocAlgebra.lift_of_apply, NonUnitalAlgHom.comp_apply, NonUnitalAlgHom.coe_codRestrict, Unitization.lift_apply, FreeNonUnitalNonAssocAlgebra.hom_ext_iff, NonUnitalSubalgebra.map_id, NonUnitalSubalgebra.range_val, NonUnitalAlgHom.snd_toFun, LieHom.toNonUnitalAlgHom_injective, FreeNonUnitalNonAssocAlgebra.lift_comp_of, NonUnitalAlgHom.coe_to_distribMulActionHom
NonUnitalAlgHomClass 📖	MathDef	4 math math: WeakDual.CharacterSpace.instNonUnitalAlgHomClass, instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass, AlgHom.instNonUnitalAlgHomClassOfAlgHomClass, NonUnitalStarAlgHom.instNonUnitalAlgHomClass
NonUnitalAlgSemiHomClass 📖	CompData	1 math math: NonUnitalAlgHom.instNonUnitalAlgSemiHomClass
«term_→ₙₐ[_]_» 📖	CompOp	—
«term_→ₙₐ_» 📖	CompOp	—
«term_→ₛₙₐ[_]_» 📖	CompOp	—

---

← Back to Index