Basic

📁 Source: Mathlib/Algebra/MonoidAlgebra/Basic.lean

Statistics

Metric	Count
Definitions algebra, algebraAddMonoidAlgebra, commAlgEquiv, curryAlgEquiv, domCongr, liftMagma, liftNCAlgHom, mapDomainAlgHom, mapDomainNonUnitalAlgHom, mapRangeAlgEquiv, mapRangeAlgHom, singleZeroAlgHom, toMultiplicativeAlgEquiv, uniqueAlgEquiv, linearMap, algebra, algebraMonoidAlgebra, commAlgEquiv, curryAlgEquiv, domCongr, equivariantOfLinearOfComm, liftMagma, liftNCAlgHom, mapDomainAlgHom, mapDomainNonUnitalAlgHom, mapRangeAlgEquiv, mapRangeAlgHom, singleOneAlgHom, toAdditiveAlgEquiv, uniqueAlgEquiv	30
Theorems algHom_ext, algHom_ext', algHom_ext'_iff, algHom_ext_iff, algebraMap_def, coe_algebraMap, coe_liftNCAlgHom, commAlgEquiv_single_single, curryAlgEquiv_single, curryAlgEquiv_symm_single, domCongr_apply, domCongr_comp_lsingle, domCongr_refl, domCongr_single, domCongr_support, domCongr_symm, domCongr_toAlgHom, isLocalHom_algebraMap, isLocalHom_singleZeroAlgHom, liftMagma_apply_apply, liftMagma_symm_apply, lift_apply, lift_apply', lift_def, lift_mapRangeRingHom_algebraMap, lift_of, lift_of', lift_single, lift_symm_apply, lift_unique, lift_unique', mapDomainAlgHom_apply, mapDomainAlgHom_comp, mapDomainAlgHom_id, mapDomainNonUnitalAlgHom_apply, mapDomainRingHom_comp_algebraMap, mapDomain_algebraMap, mapRangeAlgEquiv_apply, mapRangeAlgEquiv_trans, mapRangeAlgHom_apply, mapRangeAlgHom_single, mapRangeRingHom_comp_algebraMap, nonUnitalAlgHom_ext, nonUnitalAlgHom_ext', nonUnitalAlgHom_ext'_iff, singleZeroAlgHom_apply, symm_commAlgEquiv, symm_mapRangeAlgEquiv, toRingHom_mapRangeAlgHom, vaddAssocClass_addMonoidAlgebra, linearMap_apply, algHom_ext, algHom_ext', algHom_ext'_iff, algebraMap_def, coe_algebraMap, coe_liftNCAlgHom, commAlgEquiv_single_single, curryAlgEquiv_single, curryAlgEquiv_symm_single, domCongr_apply, domCongr_comp_lsingle, domCongr_refl, domCongr_single, domCongr_support, domCongr_symm, domCongr_toAlgHom, equivariantOfLinearOfComm_apply, isLocalHom_algebraMap, isLocalHom_singleOneAlgHom, isScalarTower_monoidAlgebra, liftMagma_apply_apply, liftMagma_symm_apply, lift_apply, lift_apply', lift_def, lift_mapRangeRingHom_algebraMap, lift_of, lift_single, lift_symm_apply, lift_unique, lift_unique', mapDomainAlgHom_apply, mapDomainAlgHom_comp, mapDomainAlgHom_id, mapDomainNonUnitalAlgHom_apply, mapDomainRingHom_comp_algebraMap, mapDomain_algebraMap, mapRangeAlgEquiv_apply, mapRangeAlgEquiv_trans, mapRangeAlgHom_apply, mapRangeAlgHom_single, mapRangeRingHom_comp_algebraMap, nonUnitalAlgHom_ext, nonUnitalAlgHom_ext', nonUnitalAlgHom_ext'_iff, singleOneAlgHom_apply, single_algebraMap_eq_algebraMap_mul_of, single_eq_algebraMap_mul_of, symm_commAlgEquiv, symm_mapRangeAlgEquiv, toRingHom_mapRangeAlgHom	102
Total	132

AddMonoidAlgebra

Definitions

Name	Category	Theorems
algebra 📖	CompOp	82 math math: mapRangeAlgEquiv_trans, lift_apply', domCongr_comp_lsingle, symm_mapRangeAlgEquiv, algHom_ext'_iff, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, mapRangeAlgHom_single, domCongr_toAlgHom, lift_mapRangeRingHom_algebraMap, mapDomainBialgHom_id, mapDomainAlgHom_id, mapRangeRingHom_comp_algebraMap, LaurentPolynomial.algebraMap_apply, mapDomainRingHom_comp_algebraMap, mapDomainBialgHom_mapDomainBialgHom, BoundedContinuousFunction.charAlgHom_apply, domCongr_refl, decomposeAux_coe, mvPolynomial_aeval_of_surjective_of_closure, tensorEquiv.invFun_tmul, Polynomial.ofFinsupp_algebraMap, commAlgEquiv_single_single, isLocalHom_algebraMap, lift_apply, domCongr_single, mapDomainBialgHom_apply, coe_algebraMap, mapRangeAlgEquiv_apply, finiteType_of_fg, addMonoidAlgebraAlgEquivDirectSum_symm_apply, finiteType_iff_group_fg, instIsPushout, instIsPushout', lift_single, mapDomainAlgHom_apply, lift_symm_apply, coe_liftNCAlgHom, lift_of, LaurentPolynomial.C_eq_algebraMap, mapDomain_algebraMap, exists_finset_adjoin_eq_top, lift_unique', toRingHom_mapRangeAlgHom, tensorEquiv_tmul, Polynomial.toFinsupp_algebraMap, LaurentPolynomial.invert_symm, symm_commAlgEquiv, mapDomainAlgHom_comp, tensorEquiv_symm_single, lift_of', mem_adjoin_support, Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp, domCongr_support, curryAlgEquiv_symm_single, domCongr_symm, algHom_ext_iff, LaurentPolynomial.invert_apply, mapDomainBialgHom_comp, scalarTensorEquiv_symm_single, Polynomial.toFinsuppIsoAlg_apply, finiteType_iff_fg, domCongr_apply, decomposeAux_single, decomposeAux_eq_decompose, lift_unique, lift_def, singleZeroAlgHom_apply, Polynomial.coe_toLaurentAlg, scalarTensorEquiv_tmul, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, Polynomial.toLaurentAlg_apply, LaurentPolynomial.toLaurent_reverse, addMonoidAlgebraAlgEquivDirectSum_apply, isLocalHom_singleZeroAlgHom, LaurentPolynomial.invert_C, curryAlgEquiv_single, mapRangeAlgHom_apply, LaurentPolynomial.invert_comp_C, freeAlgebra_lift_of_surjective_of_closure, LaurentPolynomial.invert_T, vaddAssocClass_addMonoidAlgebra, LaurentPolynomial.involutive_invert
algebraAddMonoidAlgebra 📖	CompOp	4 math math: algebraMap_def, instIsPushout, instIsPushout', vaddAssocClass_addMonoidAlgebra
commAlgEquiv 📖	CompOp	2 math math: commAlgEquiv_single_single, symm_commAlgEquiv
curryAlgEquiv 📖	CompOp	2 math math: curryAlgEquiv_symm_single, curryAlgEquiv_single
domCongr 📖	CompOp	7 math math: domCongr_comp_lsingle, domCongr_toAlgHom, domCongr_refl, domCongr_single, domCongr_support, domCongr_symm, domCongr_apply
liftMagma 📖	CompOp	2 math math: liftMagma_apply_apply, liftMagma_symm_apply
liftNCAlgHom 📖	CompOp	1 math math: coe_liftNCAlgHom
mapDomainAlgHom 📖	CompOp	4 math math: domCongr_toAlgHom, mapDomainAlgHom_id, mapDomainAlgHom_apply, mapDomainAlgHom_comp
mapDomainNonUnitalAlgHom 📖	CompOp	1 math math: mapDomainNonUnitalAlgHom_apply
mapRangeAlgEquiv 📖	CompOp	3 math math: mapRangeAlgEquiv_trans, symm_mapRangeAlgEquiv, mapRangeAlgEquiv_apply
mapRangeAlgHom 📖	CompOp	6 math math: mapRangeAlgHom_single, mapRangeAlgEquiv_apply, toRingHom_mapRangeAlgHom, tensorEquiv_tmul, scalarTensorEquiv_tmul, mapRangeAlgHom_apply
singleZeroAlgHom 📖	CompOp	2 math math: singleZeroAlgHom_apply, isLocalHom_singleZeroAlgHom
toMultiplicativeAlgEquiv 📖	CompOp	—
uniqueAlgEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	—	AlgHom.toLinearMap_injective lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids
algHom_ext' 📖	—	MonoidHom.comp Multiplicative AddMonoidAlgebra CommSemiring.toSemiring MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring MonoidHomClass.toMonoidHom AlgHom semiring algebra Algebra.id AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass of	—	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algHom_ext DFunLike.congr_fun
algHom_ext'_iff 📖	mathematical	—	MonoidHom.comp Multiplicative AddMonoidAlgebra CommSemiring.toSemiring MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring MonoidHomClass.toMonoidHom AlgHom semiring algebra Algebra.id AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass of	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algHom_ext'
algHom_ext_iff 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	algHom_ext
algebraMap_def 📖	mathematical	—	algebraMap AddMonoidAlgebra CommSemiring.toSemiring commSemiring semiring AddCommMonoid.toAddMonoid algebraAddMonoidAlgebra mapRangeRingHom	—	—
coe_algebraMap 📖	mathematical	—	DFunLike.coe RingHom AddMonoidAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap algebra single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—
coe_liftNCAlgHom 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom AlgHom.funLike MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike	AddMonoidAlgebra semiring algebra liftNCAlgHom AddMonoidHom AddZeroClass.toAddZero AddCommMonoid.toAddMonoid addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulActionSemiHomClass.toAddMonoidHomClass Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id Module.toDistribMulAction Algebra.toModule NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass	—	—
commAlgEquiv_single_single 📖	mathematical	—	DFunLike.coe AlgEquiv AddMonoidAlgebra semiring algebra AlgEquiv.instFunLike commAlgEquiv single	—	commRingEquiv_single_single
curryAlgEquiv_single 📖	mathematical	—	DFunLike.coe AlgEquiv AddMonoidAlgebra semiring Prod.instAddMonoid algebra AlgEquiv.instFunLike curryAlgEquiv single	—	curryRingEquiv_single
curryAlgEquiv_symm_single 📖	mathematical	—	DFunLike.coe AlgEquiv AddMonoidAlgebra semiring Prod.instAddMonoid algebra AlgEquiv.instFunLike AlgEquiv.symm curryAlgEquiv single	—	Finsupp.uncurry_single
domCongr_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike AlgEquiv AddMonoidAlgebra semiring algebra AlgEquiv.instFunLike domCongr AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm	—	mapDomainRingEquiv_apply
domCongr_comp_lsingle 📖	mathematical	—	LinearMap.comp AddMonoidAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Algebra.toModule algebra RingHom.id RingHomCompTriple.ids AlgEquiv.toLinearMap domCongr lsingle DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass EquivLike.toFunLike AddEquiv.instEquivLike	—	LinearMap.ext RingHomCompTriple.ids ext domCongr_single
domCongr_refl 📖	mathematical	—	domCongr AddEquiv.refl AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AlgEquiv.refl AddMonoidAlgebra semiring algebra	—	AlgEquiv.ext ext domCongr_apply
domCongr_single 📖	mathematical	—	DFunLike.coe AlgEquiv AddMonoidAlgebra semiring algebra AlgEquiv.instFunLike domCongr single AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass EquivLike.toFunLike AddEquiv.instEquivLike	—	mapDomainRingEquiv_single
domCongr_support 📖	mathematical	—	Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgEquiv AddMonoidAlgebra semiring algebra AlgEquiv.instFunLike domCongr Finset.map Equiv.toEmbedding EquivLike.toEquiv AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddEquiv.instEquivLike	—	Finset.ext Finsupp.mem_support_iff domCongr_apply Finset.mem_map_equiv
domCongr_symm 📖	mathematical	—	AlgEquiv.symm AddMonoidAlgebra semiring algebra domCongr AddEquiv.symm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—
domCongr_toAlgHom 📖	mathematical	—	AlgEquiv.toAlgHom AddMonoidAlgebra semiring algebra domCongr mapDomainAlgHom AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass	—	—
isLocalHom_algebraMap 📖	mathematical	—	IsLocalHom AddMonoidAlgebra RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike algebraMap algebra	—	IsUnit.of_map IsLocalHom.map_nonunit isLocalHom_singleZeroAlgHom
isLocalHom_singleZeroAlgHom 📖	mathematical	—	IsLocalHom AddMonoidAlgebra AlgHom semiring algebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike singleZeroAlgHom	—	IsLocalHom.map_nonunit isLocalHom_singleZeroRingHom
liftMagma_apply_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AddMonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike Equiv MulHom Multiplicative Multiplicative.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib EquivLike.toFunLike Equiv.instEquivLike liftMagma Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulHom.funLike Multiplicative.ofAdd	—	—
liftMagma_symm_apply 📖	mathematical	—	DFunLike.coe Equiv NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AddMonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MulHom Multiplicative Multiplicative.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftMagma MulHom.comp NonUnitalAlgHom.toMulHom ofMagma	—	—
lift_apply 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toSMul MonoidHom.instFunLike Multiplicative.ofAdd	—	Algebra.smul_def
lift_apply' 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap MonoidHom.instFunLike Multiplicative.ofAdd	—	—
lift_def 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift AddMonoidHom AddZeroClass.toAddZero AddCommMonoid.toAddMonoid addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom RingHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHom.instFunLike RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass algebraMap MonoidHom.instFunLike	—	—
lift_mapRangeRingHom_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift RingHom nonAssocSemiring RingHom.instFunLike mapRangeRingHom algebraMap	—	Finsupp.induction map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass mapRangeRingHom_single SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass lift_single algebraMap_smul
lift_of 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift nonAssocSemiring MonoidHom.instFunLike of	—	MonoidAlgebra.lift_of
lift_of' 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift of' MonoidHom.instFunLike Multiplicative.ofAdd	—	lift_of
lift_single 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift single Algebra.toSMul MonoidHom.instFunLike Multiplicative.ofAdd	—	MonoidAlgebra.lift_single
lift_symm_apply 📖	mathematical	—	DFunLike.coe MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.instFunLike Equiv AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift AlgHom.funLike single Multiplicative.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
lift_unique 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toSMul single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass lift_unique' lift_apply
lift_unique' 📖	mathematical	—	DFunLike.coe Equiv MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AlgHom AddMonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike lift MonoidHom.comp nonAssocSemiring MonoidHomClass.toMonoidHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass of	—	Equiv.apply_symm_apply
mapDomainAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra semiring algebra AlgHom.funLike mapDomainAlgHom mapDomain AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	—
mapDomainAlgHom_comp 📖	mathematical	—	mapDomainAlgHom AddMonoidHom.comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass AlgHom.comp AddMonoidAlgebra semiring algebra	—	AlgHom.ext ext Finsupp.mapDomain_comp
mapDomainAlgHom_id 📖	mathematical	—	mapDomainAlgHom AddMonoidHom.id AddZeroClass.toAddZero AddMonoid.toAddZeroClass AlgHom.id AddMonoidAlgebra semiring algebra	—	AlgHom.ext ext Finsupp.mapDomain_id
mapDomainNonUnitalAlgHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AddMonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule NonUnitalAlgHom.instFunLike mapDomainNonUnitalAlgHom MulHom.toFun Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalRingHom.toMulHom mapDomainNonUnitalRingHom	—	—
mapDomainRingHom_comp_algebraMap 📖	mathematical	—	RingHom.comp AddMonoidAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring nonAssocSemiring AddMonoid.toAddZeroClass mapDomainRingHom algebraMap semiring algebra	—	RingHom.ext ext Finsupp.mapDomain_single map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
mapDomain_algebraMap 📖	mathematical	—	mapDomain DFunLike.coe RingHom AddMonoidAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap algebra	—	mapDomain_single map_zero AddMonoidHomClass.toZeroHomClass
mapRangeAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv AddMonoidAlgebra semiring algebra AlgEquiv.instFunLike mapRangeAlgEquiv OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.toOneHom RingHom.toMonoidHom AlgHom.toRingHom mapRangeAlgHom AlgHomClass.toAlgHom	—	—
mapRangeAlgEquiv_trans 📖	mathematical	—	mapRangeAlgEquiv AlgEquiv.trans AddMonoidAlgebra semiring algebra	—	AlgEquiv.ext ext AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mapRangeRingHom_comp mapRangeRingHom_apply
mapRangeAlgHom_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike AlgHom AddMonoidAlgebra semiring algebra AlgHom.funLike mapRangeAlgHom	—	mapRangeRingHom_apply
mapRangeAlgHom_single 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra semiring algebra AlgHom.funLike mapRangeAlgHom single	—	ext mapRangeAlgHom_apply single_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
mapRangeRingHom_comp_algebraMap 📖	mathematical	—	RingHom.comp AddMonoidAlgebra CommSemiring.toSemiring Semiring.toNonAssocSemiring nonAssocSemiring AddMonoid.toAddZeroClass mapRangeRingHom algebraMap semiring algebra Algebra.id	—	RingHom.ext ext CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId mapRangeRingHom_single
nonUnitalAlgHom_ext 📖	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AddMonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	NonUnitalAlgHom.to_distribMulActionHom_injective Finsupp.distribMulActionHom_ext' NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass DistribMulActionHom.ext_ring MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId
nonUnitalAlgHom_ext' 📖	—	MulHom.comp Multiplicative AddMonoidAlgebra Multiplicative.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring NonUnitalAlgHom.toMulHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ofMagma	—	—	nonUnitalAlgHom_ext DFunLike.congr_fun
nonUnitalAlgHom_ext'_iff 📖	mathematical	—	MulHom.comp Multiplicative AddMonoidAlgebra Multiplicative.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring NonUnitalAlgHom.toMulHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ofMagma	—	nonUnitalAlgHom_ext'
singleZeroAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom AddMonoidAlgebra semiring algebra AlgHom.funLike singleZeroAlgHom single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—
symm_commAlgEquiv 📖	mathematical	—	AlgEquiv.symm AddMonoidAlgebra semiring algebra commAlgEquiv	—	—
symm_mapRangeAlgEquiv 📖	mathematical	—	AlgEquiv.symm AddMonoidAlgebra semiring algebra mapRangeAlgEquiv	—	—
toRingHom_mapRangeAlgHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom AddMonoidAlgebra semiring algebra AlgHom.funLike nonAssocSemiring AddMonoid.toAddZeroClass AlgHomClass.toRingHomClass AlgHom.algHomClass mapRangeAlgHom mapRangeRingHom AlgHom.toRingHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
vaddAssocClass_addMonoidAlgebra 📖	mathematical	—	IsScalarTower AddMonoidAlgebra CommSemiring.toSemiring Algebra.toSMul semiring AddCommMonoid.toAddMonoid algebra commSemiring algebraAddMonoidAlgebra	—	IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap

MonoidAlgebra

Definitions

Name	Category	Theorems
algebra 📖	CompOp	78 math math: finiteType_of_fg, isLocalHom_algebraMap, Representation.asAlgebraHom_single, algHom_ext'_iff, tensorEquiv.invFun_tmul, domCongr_toAlgHom, Rep.to_Module_monoidAlgebra_map_aux, mem_adjoin_support, Representation.asAlgebraHom_def, lift_symm_apply, coe_liftNCAlgHom, Representation.smul_ofModule_asModule, instIsPushout, mapDomainBialgHom_comp, coe_algebraMap, mapDomain_algebraMap, mapDomainBialgHom_mapDomainBialgHom, mapRangeAlgHom_single, mapRangeAlgEquiv_trans, mvPolynomial_aeval_of_surjective_of_closure, domCongr_single, toRingHom_mapRangeAlgHom, scalarTensorEquiv_tmul, single_algebraMap_eq_algebraMap_mul_of, mapDomainAlgHom_id, mapDomainAlgHom_comp, Subrepresentation.mem_asSubmodule'_iff, Representation.asModuleEquiv_symm_map_smul, mapRangeAlgHom_apply, symm_mapRangeAlgEquiv, lift_unique, tensorEquiv_symm_single, lift_apply', Subrepresentation.submoduleSubrepresentationOrderIso_apply, mapDomainBialgHom_apply, mapRangeAlgEquiv_apply, freeAlgebra_lift_of_surjective_of_closure, Representation.asAlgebraHom_single_one, mapRangeRingHom_comp_algebraMap, Representation.isSimpleModule_iff_irreducible_ofModule, Representation.instIsScalarTowerMonoidAlgebraAsModule, commAlgEquiv_single_single, isScalarTower_monoidAlgebra, isLocalHom_singleOneAlgHom, finiteType_iff_fg, exists_finset_adjoin_eq_top, Representation.ofModule_asModule_act, tensorEquiv_tmul, Representation.asAlgebraHom_of, finiteType_iff_group_fg, domCongr_comp_lsingle, instIsPushout', domCongr_symm, scalarTensorEquiv_symm_single, lift_apply, lift_mapRangeRingHom_algebraMap, Representation.ofModule_asAlgebraHom_apply_apply, symm_commAlgEquiv, curryAlgEquiv_symm_single, single_eq_algebraMap_mul_of, domCongr_support, Representation.asModuleEquiv_map_smul, singleOneAlgHom_apply, lift_def, Representation.is_simple_module_iff_irreducible_ofModule, Subrepresentation.mem_ofSubmodule_iff, mapDomainAlgHom_apply, mapDomainRingHom_comp_algebraMap, Representation.asAlgebraHom_mem_of_forall_mem, domCongr_refl, domCongr_apply, mapDomainBialgHom_id, lift_single, curryAlgEquiv_single, Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule, Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply, lift_of, lift_unique'
algebraMonoidAlgebra 📖	CompOp	4 math math: instIsPushout, isScalarTower_monoidAlgebra, instIsPushout', algebraMap_def
commAlgEquiv 📖	CompOp	2 math math: commAlgEquiv_single_single, symm_commAlgEquiv
curryAlgEquiv 📖	CompOp	2 math math: curryAlgEquiv_symm_single, curryAlgEquiv_single
domCongr 📖	CompOp	7 math math: domCongr_toAlgHom, domCongr_single, domCongr_comp_lsingle, domCongr_symm, domCongr_support, domCongr_refl, domCongr_apply
equivariantOfLinearOfComm 📖	CompOp	1 math math: equivariantOfLinearOfComm_apply
liftMagma 📖	CompOp	2 math math: liftMagma_apply_apply, liftMagma_symm_apply
liftNCAlgHom 📖	CompOp	1 math math: coe_liftNCAlgHom
mapDomainAlgHom 📖	CompOp	4 math math: domCongr_toAlgHom, mapDomainAlgHom_id, mapDomainAlgHom_comp, mapDomainAlgHom_apply
mapDomainNonUnitalAlgHom 📖	CompOp	1 math math: mapDomainNonUnitalAlgHom_apply
mapRangeAlgEquiv 📖	CompOp	3 math math: mapRangeAlgEquiv_trans, symm_mapRangeAlgEquiv, mapRangeAlgEquiv_apply
mapRangeAlgHom 📖	CompOp	6 math math: mapRangeAlgHom_single, toRingHom_mapRangeAlgHom, scalarTensorEquiv_tmul, mapRangeAlgHom_apply, mapRangeAlgEquiv_apply, tensorEquiv_tmul
singleOneAlgHom 📖	CompOp	2 math math: isLocalHom_singleOneAlgHom, singleOneAlgHom_apply
toAdditiveAlgEquiv 📖	CompOp	—
uniqueAlgEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	—	AlgHom.toLinearMap_injective lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids
algHom_ext' 📖	—	MonoidHom.comp MonoidAlgebra CommSemiring.toSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring MonoidHomClass.toMonoidHom AlgHom semiring algebra Algebra.id AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass of	—	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algHom_ext DFunLike.congr_fun
algHom_ext'_iff 📖	mathematical	—	MonoidHom.comp MonoidAlgebra CommSemiring.toSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring MonoidHomClass.toMonoidHom AlgHom semiring algebra Algebra.id AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass of	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algHom_ext'
algebraMap_def 📖	mathematical	—	algebraMap MonoidAlgebra CommSemiring.toSemiring commSemiring semiring CommMonoid.toMonoid algebraMonoidAlgebra mapRangeRingHom	—	—
coe_algebraMap 📖	mathematical	—	DFunLike.coe RingHom MonoidAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap algebra single MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
coe_liftNCAlgHom 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom AlgHom.funLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike	MonoidAlgebra semiring algebra liftNCAlgHom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulActionSemiHomClass.toAddMonoidHomClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id Module.toDistribMulAction Algebra.toModule NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass	—	—
commAlgEquiv_single_single 📖	mathematical	—	DFunLike.coe AlgEquiv MonoidAlgebra semiring algebra AlgEquiv.instFunLike commAlgEquiv single	—	commRingEquiv_single_single
curryAlgEquiv_single 📖	mathematical	—	DFunLike.coe AlgEquiv MonoidAlgebra semiring Prod.instMonoid algebra AlgEquiv.instFunLike curryAlgEquiv single	—	curryRingEquiv_single
curryAlgEquiv_symm_single 📖	mathematical	—	DFunLike.coe AlgEquiv MonoidAlgebra semiring Prod.instMonoid algebra AlgEquiv.instFunLike AlgEquiv.symm curryAlgEquiv single	—	Finsupp.uncurry_single
domCongr_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike AlgEquiv MonoidAlgebra semiring algebra AlgEquiv.instFunLike domCongr MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm	—	mapDomainRingEquiv_apply
domCongr_comp_lsingle 📖	mathematical	—	LinearMap.comp MonoidAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Algebra.toModule algebra RingHom.id RingHomCompTriple.ids AlgEquiv.toLinearMap domCongr lsingle DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	—	LinearMap.ext RingHomCompTriple.ids ext domCongr_single
domCongr_refl 📖	mathematical	—	domCongr MulEquiv.refl MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AlgEquiv.refl MonoidAlgebra semiring algebra	—	AlgEquiv.ext ext domCongr_apply
domCongr_single 📖	mathematical	—	DFunLike.coe AlgEquiv MonoidAlgebra semiring algebra AlgEquiv.instFunLike domCongr single MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	—	mapDomainRingEquiv_single
domCongr_support 📖	mathematical	—	Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgEquiv MonoidAlgebra semiring algebra AlgEquiv.instFunLike domCongr Finset.map Equiv.toEmbedding EquivLike.toEquiv MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulEquiv.instEquivLike	—	Finset.ext domCongr_apply
domCongr_symm 📖	mathematical	—	AlgEquiv.symm MonoidAlgebra semiring algebra domCongr MulEquiv.symm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
domCongr_toAlgHom 📖	mathematical	—	AlgEquiv.toAlgHom MonoidAlgebra semiring algebra domCongr mapDomainAlgHom MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass	—	—
equivariantOfLinearOfComm_apply 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike MonoidAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Module.toDistribMulAction single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	nonAssocSemiring Monoid.toMulOneClass equivariantOfLinearOfComm	—	—
isLocalHom_algebraMap 📖	mathematical	—	IsLocalHom MonoidAlgebra RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike algebraMap algebra	—	IsUnit.of_map IsLocalHom.map_nonunit isLocalHom_singleOneAlgHom
isLocalHom_singleOneAlgHom 📖	mathematical	—	IsLocalHom MonoidAlgebra AlgHom semiring algebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike singleOneAlgHom	—	IsLocalHom.map_nonunit isLocalHom_singleOneRingHom
isScalarTower_monoidAlgebra 📖	mathematical	—	IsScalarTower MonoidAlgebra CommSemiring.toSemiring Algebra.toSMul semiring CommMonoid.toMonoid algebra commSemiring algebraMonoidAlgebra	—	IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap
liftMagma_apply_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike Equiv MulHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib EquivLike.toFunLike Equiv.instEquivLike liftMagma Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulHom.funLike	—	—
liftMagma_symm_apply 📖	mathematical	—	DFunLike.coe Equiv NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MulHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib EquivLike.toFunLike Equiv.instEquivLike Equiv.symm liftMagma MulHom.comp NonUnitalAlgHom.toMulHom ofMagma	—	—
lift_apply 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toSMul MonoidHom.instFunLike	—	Algebra.smul_def
lift_apply' 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap MonoidHom.instFunLike	—	—
lift_def 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidHom.instFunLike liftNC AddMonoidHomClass.toAddMonoidHom RingHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHom.instFunLike RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass algebraMap MonoidHom.instFunLike	—	—
lift_mapRangeRingHom_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift RingHom nonAssocSemiring RingHom.instFunLike mapRangeRingHom algebraMap	—	Finsupp.induction map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass mapRangeRingHom_single SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass lift_single algebraMap_smul
lift_of 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift nonAssocSemiring MonoidHom.instFunLike of	—	lift_single one_smul
lift_single 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike lift single Algebra.toSMul MonoidHom.instFunLike	—	RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass lift_def liftNC_single Algebra.smul_def AddMonoidHom.coe_coe
lift_symm_apply 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.instFunLike Equiv AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift AlgHom.funLike single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
lift_unique 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id AlgHom.funLike Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toSMul single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass lift_unique' lift_apply
lift_unique' 📖	mathematical	—	DFunLike.coe Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AlgHom MonoidAlgebra CommSemiring.toSemiring semiring algebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike lift MonoidHom.comp nonAssocSemiring MonoidHomClass.toMonoidHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass of	—	Equiv.apply_symm_apply
mapDomainAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra semiring algebra AlgHom.funLike mapDomainAlgHom mapDomain MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	—
mapDomainAlgHom_comp 📖	mathematical	—	mapDomainAlgHom MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass AlgHom.comp MonoidAlgebra semiring algebra	—	AlgHom.ext ext Finsupp.mapDomain_comp
mapDomainAlgHom_id 📖	mathematical	—	mapDomainAlgHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass AlgHom.id MonoidAlgebra semiring algebra	—	AlgHom.ext ext Finsupp.mapDomain_id
mapDomainNonUnitalAlgHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule NonUnitalAlgHom.instFunLike mapDomainNonUnitalAlgHom MulHom.toFun Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalRingHom.toMulHom mapDomainNonUnitalRingHom	—	—
mapDomainRingHom_comp_algebraMap 📖	mathematical	—	RingHom.comp MonoidAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring nonAssocSemiring Monoid.toMulOneClass mapDomainRingHom algebraMap semiring algebra	—	RingHom.ext ext Finsupp.mapDomain_single map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
mapDomain_algebraMap 📖	mathematical	—	mapDomain DFunLike.coe RingHom MonoidAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap algebra	—	mapDomain_single map_one MonoidHomClass.toOneHomClass
mapRangeAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MonoidAlgebra semiring algebra AlgEquiv.instFunLike mapRangeAlgEquiv OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidHom.toOneHom RingHom.toMonoidHom AlgHom.toRingHom mapRangeAlgHom AlgHomClass.toAlgHom	—	—
mapRangeAlgEquiv_trans 📖	mathematical	—	mapRangeAlgEquiv AlgEquiv.trans MonoidAlgebra semiring algebra	—	AlgEquiv.ext ext AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mapRangeRingHom_comp mapRangeRingHom_apply
mapRangeAlgHom_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike AlgHom MonoidAlgebra semiring algebra AlgHom.funLike mapRangeAlgHom	—	mapRangeRingHom_apply
mapRangeAlgHom_single 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra semiring algebra AlgHom.funLike mapRangeAlgHom single	—	ext mapRangeAlgHom_apply single_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
mapRangeRingHom_comp_algebraMap 📖	mathematical	—	RingHom.comp MonoidAlgebra CommSemiring.toSemiring Semiring.toNonAssocSemiring nonAssocSemiring Monoid.toMulOneClass mapRangeRingHom algebraMap semiring algebra Algebra.id	—	RingHom.ext ext CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId mapRangeRingHom_single
nonUnitalAlgHom_ext 📖	—	DFunLike.coe NonUnitalAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidAlgebra nonUnitalNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalAlgHom.instFunLike_1 single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	NonUnitalAlgHom.to_distribMulActionHom_injective Finsupp.distribMulActionHom_ext' NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass DistribMulActionHom.ext_ring MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId
nonUnitalAlgHom_ext' 📖	—	MulHom.comp MonoidAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring NonUnitalAlgHom.toMulHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ofMagma	—	—	nonUnitalAlgHom_ext DFunLike.congr_fun
nonUnitalAlgHom_ext'_iff 📖	mathematical	—	MulHom.comp MonoidAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib nonUnitalNonAssocSemiring NonUnitalAlgHom.toMulHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring distribMulAction Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ofMagma	—	nonUnitalAlgHom_ext'
singleOneAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra semiring algebra AlgHom.funLike singleOneAlgHom single MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
single_algebraMap_eq_algebraMap_mul_of 📖	mathematical	—	single DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap MonoidAlgebra instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass semiring algebra MonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring MonoidHom.instFunLike of	—	single_mul_single one_mul mul_one
single_eq_algebraMap_mul_of 📖	mathematical	—	single CommSemiring.toSemiring MonoidAlgebra instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike algebraMap algebra Algebra.id MonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring MonoidHom.instFunLike of	—	single_mul_single one_mul mul_one
symm_commAlgEquiv 📖	mathematical	—	AlgEquiv.symm MonoidAlgebra semiring algebra commAlgEquiv	—	—
symm_mapRangeAlgEquiv 📖	mathematical	—	AlgEquiv.symm MonoidAlgebra semiring algebra mapRangeAlgEquiv	—	—
toRingHom_mapRangeAlgHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom MonoidAlgebra semiring algebra AlgHom.funLike nonAssocSemiring Monoid.toMulOneClass AlgHomClass.toRingHomClass AlgHom.algHomClass mapRangeAlgHom mapRangeRingHom AlgHom.toRingHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass

MonoidAlgebra.GroupSMul

Definitions

Name	Category	Theorems
linearMap 📖	CompOp	1 math math: linearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMap MonoidAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction MonoidAlgebra.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—

---

← Back to Index