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	11 math math: range_comp_le_range, Unitization.algHom_ext'_iff, 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	79 math math: map_smul, congr_fun, one_apply, NonUnitalSubalgebraClass.coe_subtype, range_comp_le_range, coe_lmul_eq_mul, NonUnitalSubalgebra.inclusion_mk, NonUnitalSubalgebra.inclusion_right, FreeNonUnitalNonAssocAlgebra.of_comp_lift, 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_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, FreeLieAlgebra.liftAux_spec, addHomMk_coe, map_add, LinearMap.nonUnitalAlgHom_comp_convMul_distrib, comp_mul', coe_inl, prod_toFun, NonUnitalAlgebra.map_top, toAlgHom_apply, toMulHom_eq_coe, coe_id, 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 NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass instNonUnitalAlgSemiHomClass	—	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	inverse	—	—
coe_inverse' 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike 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	NonUnitalAlgHom instFunLike_1	—	—
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 NonUnitalAlgSemiHomClass.toMulHomClass instNonUnitalAlgSemiHomClass	—	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 DistribMulActionHom.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 📖	—	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	—	—	—
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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom instFunLike_1 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 AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalAlgHom instFunLike_1 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	105 math math: NonUnitalAlgHom.map_smul, NonUnitalAlgHom.congr_fun, MonoidAlgebra.liftMagma_apply_apply, 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.inclusion_right, FreeNonUnitalNonAssocAlgebra.of_comp_lift, 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_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, FreeLieAlgebra.liftAux_spec, NonUnitalAlgHom.addHomMk_coe, Unitization.lift_symm_apply, NonUnitalAlgHom.map_add, AddMonoidAlgebra.liftMagma_apply_apply, NonUnitalAlgHom.toFun_eq_coe, MonoidAlgebra.liftMagma_symm_apply, AddMonoidAlgebra.liftMagma_symm_apply, 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, 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