Basic

📁 Source: Mathlib/RepresentationTheory/Basic.lean

Statistics

Metric	Count
Definitions IsTrivial, asAlgebraHom, asGroupHom, asModule, asModuleEquiv, diagonal, directSum, dual, finsupp, finsuppLEquivFreeAsModule, free, freeAsModuleBasis, instAddCommGroupAsModule, instAddCommGroupAsModuleFinsuppFree, instAddCommMonoidAsModule, instHMulMonoidAlgebraAsModuleFinsuppOfMulAction, instInhabitedAsModule, instModuleAsModule, instModuleMonoidAlgebraAsModule, leftRegular, linHom, norm, ofDistribMulAction, ofModule, ofModule', ofMulAction, ofMulActionSelfAsModuleEquiv, ofMulDistribMulAction, ofQuotient, prod, quotient, subrepresentation, tprod, trivial	34
Theorems out, apply_bijective, apply_eq_of_coe_eq, apply_eq_of_leftRegular_eq_of_generator, apply_sub_id_partialSum_eq, asAlgebraHom_def, asAlgebraHom_of, asAlgebraHom_single, asAlgebraHom_single_one, asGroupHom_apply, asModuleEquiv_map_smul, asModuleEquiv_symm_map_rho, asModuleEquiv_symm_map_smul, directSum_apply, dualTensorHom_comm, dual_apply, finsupp_apply, finsupp_single, free_asModule_free, free_single_single, instFiniteAsModule, instIsScalarTowerMonoidAlgebraAsModule, instIsTrivialTrivial, inv_self_apply, isTrivial_apply, isTrivial_def, ker_leftRegular_norm_eq, leftRegular_norm_apply, leftRegular_norm_eq_zero_iff, linHom_apply, norm_comp_self, norm_ofDistribMulAction_eq, norm_ofMulDistribMulAction_eq, norm_self_apply, ofDistribMulAction_apply_apply, ofModule_asAlgebraHom_apply_apply, ofModule_asModule_act, ofMulActionSelfAsModuleEquiv_apply, ofMulActionSelfAsModuleEquiv_symm_apply, ofMulAction_apply, ofMulAction_def, ofMulAction_self_smul_eq_mul, ofMulAction_single, ofMulDistribMulAction_apply_apply, ofQuotient_coe_apply, prod_apply_apply, quotient_apply, self_comp_norm, self_inv_apply, self_norm_apply, single_smul, smul_ofModule_asModule, smul_one_tprod_asModule, smul_tprod_one_asModule, subrepresentation_apply, tprod_apply, trivial_apply	57
Total	91

Representation

Definitions

Name	Category	Theorems
IsTrivial 📖	CompData	4 math math: instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, instIsTrivialTrivial, instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, Rep.instIsTrivialVOfCompLinearMapIdρ
asAlgebraHom 📖	CompOp	7 math math: asAlgebraHom_single, asAlgebraHom_def, asAlgebraHom_single_one, asAlgebraHom_of, ofModule_asAlgebraHom_apply_apply, asModuleEquiv_map_smul, asAlgebraHom_mem_of_forall_mem
asGroupHom 📖	CompOp	1 math math: asGroupHom_apply
asModule 📖	CompOp	23 math math: IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule, ofMulActionSelfAsModuleEquiv_symm_apply, Subrepresentation.mem_ofSubmodule'_iff, smul_ofModule_asModule, instFiniteAsModule, ofMulAction_self_smul_eq_mul, single_smul, asModuleEquiv_symm_map_smul, isSemisimpleRepresentation_iff_isSemisimpleModule_asModule, instIsScalarTowerMonoidAlgebraAsModule, Subrepresentation.mem_asSubmodule_iff, RootPairing.isSimpleModule_weylGroupRootRep, ofMulActionSelfAsModuleEquiv_apply, RootPairing.isSimpleModule_weylGroupRootRep_iff, asModuleEquiv_symm_map_rho, ofModule_asModule_act, smul_tprod_one_asModule, Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply, irreducible_iff_isSimpleModule_asModule, asModuleEquiv_map_smul, smul_one_tprod_asModule, free_asModule_free, Subrepresentation.subrepresentationSubmoduleOrderIso_apply
asModuleEquiv 📖	CompOp	8 math math: ofMulActionSelfAsModuleEquiv_symm_apply, smul_ofModule_asModule, single_smul, asModuleEquiv_symm_map_smul, ofMulActionSelfAsModuleEquiv_apply, asModuleEquiv_symm_map_rho, ofModule_asModule_act, asModuleEquiv_map_smul
diagonal 📖	CompOp	2 math math: diagonalOneEquivLeftRegular_symm_apply_single, diagonalOneEquivLeftRegular_apply_single
directSum 📖	CompOp	1 math math: directSum_apply
dual 📖	CompOp	7 math math: char_dual, Equiv.dualTensorHom_toFun, FDRep.char_dual, dual_apply, dualTensorHom_comm, Equiv.dualTensorHom_invFun, FDRep.dualTensorIsoLinHom_hom_hom
finsupp 📖	CompOp	12 math math: finsupp_apply, finsuppTensorLeft_apply_tmul, finsuppTensorRight_apply_tmul, coinvariantsFinsuppLEquiv_apply, finsuppToCoinvariants_single_mk, finsupp_single, finsuppTensorRight_symm_apply_single, finsuppTensorLeft_symm_apply_single, finsuppTensorLeft_apply_tmul_apply, coinvariantsToFinsupp_mk_single, coinvariantsFinsuppLEquiv_symm_apply, finsuppTensorRight_apply_tmul_apply
finsuppLEquivFreeAsModule 📖	CompOp	—
free 📖	CompOp	11 math math: freeLift_single_single, Rep.finsuppToCoinvariantsTensorFree_single, leftRegularTensorTrivialIsoFree_symm_apply_single_single, Rep.coinvariantsTensorFreeLEquiv_apply, freeLift_toLinearMap, free_single_single, leftRegularTensorTrivialIsoFree_apply_single_tmul_single, freeLiftLEquiv_symm_apply, free_asModule_free, freeLiftLEquiv_apply, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single
freeAsModuleBasis 📖	CompOp	—
instAddCommGroupAsModule 📖	CompOp	5 math math: IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule, isSemisimpleRepresentation_iff_isSemisimpleModule_asModule, RootPairing.isSimpleModule_weylGroupRootRep, RootPairing.isSimpleModule_weylGroupRootRep_iff, irreducible_iff_isSimpleModule_asModule
instAddCommGroupAsModuleFinsuppFree 📖	CompOp	—
instAddCommMonoidAsModule 📖	CompOp	18 math math: ofMulActionSelfAsModuleEquiv_symm_apply, Subrepresentation.mem_ofSubmodule'_iff, smul_ofModule_asModule, instFiniteAsModule, ofMulAction_self_smul_eq_mul, single_smul, asModuleEquiv_symm_map_smul, instIsScalarTowerMonoidAlgebraAsModule, Subrepresentation.mem_asSubmodule_iff, ofMulActionSelfAsModuleEquiv_apply, asModuleEquiv_symm_map_rho, ofModule_asModule_act, smul_tprod_one_asModule, Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply, asModuleEquiv_map_smul, smul_one_tprod_asModule, free_asModule_free, Subrepresentation.subrepresentationSubmoduleOrderIso_apply
instHMulMonoidAlgebraAsModuleFinsuppOfMulAction 📖	CompOp	1 math math: ofMulAction_self_smul_eq_mul
instInhabitedAsModule 📖	CompOp	—
instModuleAsModule 📖	CompOp	10 math math: ofMulActionSelfAsModuleEquiv_symm_apply, smul_ofModule_asModule, instFiniteAsModule, single_smul, asModuleEquiv_symm_map_smul, instIsScalarTowerMonoidAlgebraAsModule, ofMulActionSelfAsModuleEquiv_apply, asModuleEquiv_symm_map_rho, ofModule_asModule_act, asModuleEquiv_map_smul
instModuleMonoidAlgebraAsModule 📖	CompOp	22 math math: IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule, ofMulActionSelfAsModuleEquiv_symm_apply, Subrepresentation.mem_ofSubmodule'_iff, smul_ofModule_asModule, ofMulAction_self_smul_eq_mul, single_smul, asModuleEquiv_symm_map_smul, isSemisimpleRepresentation_iff_isSemisimpleModule_asModule, instIsScalarTowerMonoidAlgebraAsModule, Subrepresentation.mem_asSubmodule_iff, RootPairing.isSimpleModule_weylGroupRootRep, ofMulActionSelfAsModuleEquiv_apply, RootPairing.isSimpleModule_weylGroupRootRep_iff, asModuleEquiv_symm_map_rho, ofModule_asModule_act, smul_tprod_one_asModule, Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply, irreducible_iff_isSimpleModule_asModule, asModuleEquiv_map_smul, smul_one_tprod_asModule, free_asModule_free, Subrepresentation.subrepresentationSubmoduleOrderIso_apply
leftRegular 📖	CompOp	29 math math: Rep.coindToInd_of_support_subset_orbit, ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.coindToInd_indToCoind, leftRegularTensorTrivialIsoFree_symm_apply_single_single, leftRegular_norm_eq_zero_iff, coinvariantsTprodLeftRegularLEquiv_apply, Rep.coindToInd_apply, ker_leftRegular_norm_eq, Rep.indCoindIso_hom_hom_toLinearMap, FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, coinvariantsTprodLeftRegularLEquiv_symm_apply, Rep.indCoindIso_inv_hom_toLinearMap, leftRegularTensorTrivialIsoFree_apply_single_tmul_single, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, diagonalOneEquivLeftRegular_symm_apply_single, leftRegular_norm_apply, ind_mk, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.indToCoind_coindToInd, Rep.indResHomEquiv_symm_apply, leftRegularMapEquiv_symm_single, ind_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, leftRegularMapEquiv_apply, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, diagonalOneEquivLeftRegular_apply_single, IndV.hom_ext_iff, leftRegularMapEquiv_symm_apply_toFun, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
linHom 📖	CompOp	13 math math: Rep.tensorHomEquiv_apply, linHom_apply, linHom.invariantsEquivRepHom_apply, FDRep.char_linHom, linHom.invariantsEquivRepHom_symm_apply_coe, Equiv.dualTensorHom_toFun, Rep.ihom_map, char_linHom, linHom.mem_invariants_iff_comm, dualTensorHom_comm, Equiv.dualTensorHom_invFun, Rep.ihom_obj_ρ, FDRep.dualTensorIsoLinHom_hom_hom
norm 📖	CompOp	15 math math: Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, Rep.norm_comm_apply, leftRegular_norm_eq_zero_iff, norm_ofMulDistribMulAction_eq, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, norm_comp_self, ker_leftRegular_norm_eq, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, norm_ofDistribMulAction_eq, norm_self_apply, Rep.norm_apply, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, leftRegular_norm_apply, self_comp_norm, self_norm_apply
ofDistribMulAction 📖	CompOp	3 math math: ofDistribMulAction_apply_apply, norm_ofDistribMulAction_eq, groupHomology.coinvariantsKerOfIsBoundary₀_coe
ofModule 📖	CompOp	11 math math: smul_ofModule_asModule, Subrepresentation.mem_asSubmodule'_iff, Subrepresentation.submoduleSubrepresentationOrderIso_apply, isSimpleModule_iff_irreducible_ofModule, Rep.ofModuleMonoidAlgebra_obj_ρ, ofModule_asModule_act, ofModule_asAlgebraHom_apply_apply, is_simple_module_iff_irreducible_ofModule, Subrepresentation.mem_ofSubmodule_iff, isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule, Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply
ofModule' 📖	CompOp	—
ofMulAction 📖	CompOp	12 math math: ofMulActionSelfAsModuleEquiv_symm_apply, ofMulAction_apply, ofMulActionSubsingletonEquivTrivial_symm_apply, ofMulAction_single, ofMulAction_self_smul_eq_mul, ofMulActionSubsingletonEquivTrivial_apply, Rep.coindFunctorIso_inv_app_hom_toFun_coe, ofMulActionSelfAsModuleEquiv_apply, linearizeOfMulActionIso_apply, linearizeOfMulActionIso_symm_apply, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, ofMulAction_def
ofMulActionSelfAsModuleEquiv 📖	CompOp	2 math math: ofMulActionSelfAsModuleEquiv_symm_apply, ofMulActionSelfAsModuleEquiv_apply
ofMulDistribMulAction 📖	CompOp	2 math math: norm_ofMulDistribMulAction_eq, ofMulDistribMulAction_apply_apply
ofQuotient 📖	CompOp	2 math math: ofQuotient_coe_apply, Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap
prod 📖	CompOp	1 math math: prod_apply_apply
quotient 📖	CompOp	2 math math: quotient_apply, Rep.mkQ_hom_toFun
subrepresentation 📖	CompOp	2 math math: Rep.subtype_hom_toFun, subrepresentation_apply
tprod 📖	CompOp	98 math math: Rep.hom_hom_associator, IntertwiningMap.rTensor_zero, IntertwiningMap.rTensor_id, Rep.coindToInd_of_support_subset_orbit, Coinvariants.mk_inv_tmul, finsuppTensorLeft_apply_tmul, ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.coindToInd_indToCoind, Rep.of_tensor, Rep.finsuppToCoinvariantsTensorFree_single, finsuppTensorRight_apply_tmul, Coinvariants.mk_tmul_inv, leftRegularTensorTrivialIsoFree_symm_apply_single_single, LinearizeMonoidal.μ_apply_single_single, TensorProduct.assoc_symm_toLinearMap, Rep.μ_def, Rep.hom_hom_leftUnitor, IntertwiningMap.lTensor_add, tprod_apply, IntertwiningMap.tensor_add_left, LinearizeMonoidal.μ_comp_assoc, coinvariantsTprodLeftRegularLEquiv_apply, TensorProduct.rid_symm_apply, Rep.coinvariantsTensorFreeLEquiv_apply, Rep.δ_def, IntertwiningMap.tensor_smul_right, LinearizeMonoidal.μ_comp_rTensor, LinearizeMonoidal.μ_δ, IntertwiningMap.lTensor_id, IntertwiningMap.toLinearMap_rTensor, Rep.coindToInd_apply, IntertwiningMap.rTensor_comp_lTensor, char_tensor, IntertwiningMap.lTensor_zero, Rep.hom_braiding, Rep.tensor_ρ, LinearizeMonoidal.assoc_comp_δ, TensorProduct.comm_comp_rTensor, LinearizeMonoidal.rTensor_comp_δ, IntertwiningMap.tensor_add_right, LinearizeMonoidal.μ_comp_lTensor, TensorProduct.rid_apply, LinearizeMonoidal.rightUnitor_δ, Rep.hom_inv_rightUnitor, Rep.hom_hom_rightUnitor, finsuppTensorRight_symm_apply_single, IntertwiningMap.rTensor_smul, IntertwiningMap.lTensor_comp_rTensor, IntertwiningMap.toLinearMap_lTensor, Rep.indCoindIso_hom_hom_toLinearMap, smul_tprod_one_asModule, TensorProduct.toLinearMap_assoc, TensorProduct.comm_apply, LinearizeMonoidal.leftUnitor_δ, finsuppTensorLeft_symm_apply_single, IntertwiningMap.tensor_smul_left, TensorProduct.comm_comp_lTensor, coinvariantsTprodLeftRegularLEquiv_symm_apply, Equiv.dualTensorHom_toFun, IntertwiningMap.lTensor_apply, Rep.indCoindIso_inv_hom_toLinearMap, LinearizeMonoidal.lTensor_comp_δ, leftRegularTensorTrivialIsoFree_apply_single_tmul_single, LinearizeMonoidal.δ_apply_single, LinearizeMonoidal.μ_toLinearMap, LinearizeMonoidal.μ_leftUnitor, Rep.hom_inv_leftUnitor, Rep.hom_inv_associator, TensorProduct.lid_symm_apply, finsuppTensorLeft_apply_tmul_apply, LinearizeMonoidal.μ_rightUnitor, LinearizeMonoidal.δ_μ, ind_mk, TensorProduct.comm_symm, IntertwiningMap.toLinearMap_tensor, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.indToCoind_coindToInd, IntertwiningMap.lTensor_smul, IntertwiningMap.rTensor_add, Rep.indResHomEquiv_symm_apply, smul_one_tprod_asModule, TensorProduct.assoc_apply, Rep.tensorHomEquiv_symm_apply, LinearizeMonoidal.μ_apply_apply, ind_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, TensorProduct.toLinearMap_rid, Equiv.dualTensorHom_invFun, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, TensorProduct.toLinearMap_comm, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, IntertwiningMap.rTensor_apply, TensorProduct.lid_apply, finsuppTensorRight_apply_tmul_apply, IndV.hom_ext_iff, IntertwiningMap.tensor_apply, TensorProduct.toLinearMap_lid, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
trivial 📖	CompOp	34 math math: LinearizeMonoidal.ε_η, Rep.ε_def, ofMulActionSubsingletonEquivTrivial_symm_apply, leftRegularTensorTrivialIsoFree_symm_apply_single_single, Rep.hom_hom_leftUnitor, ofMulActionSubsingletonEquivTrivial_apply, TensorProduct.rid_symm_apply, LinearizeMonoidal.ε_one, linearizeTrivialIso_apply, LinearizeMonoidal.η_toLinearMap, instIsTrivialTrivial, TensorProduct.rid_apply, LinearizeMonoidal.rightUnitor_δ, Rep.hom_inv_rightUnitor, LinearizeMonoidal.η_single, Rep.hom_hom_rightUnitor, Rep.coinvariantsAdjunction_unit_app, Rep.trivialFunctor_map_hom, LinearizeMonoidal.leftUnitor_δ, LinearizeMonoidal.η_ε, leftRegularTensorTrivialIsoFree_apply_single_tmul_single, Rep.η_def, LinearizeMonoidal.μ_leftUnitor, Rep.hom_inv_leftUnitor, TensorProduct.lid_symm_apply, LinearizeMonoidal.μ_rightUnitor, Rep.invariantsAdjunction_counit_app, Rep.tensorUnit_ρ, TensorProduct.toLinearMap_rid, TensorProduct.lid_apply, trivial_apply, TensorProduct.toLinearMap_lid, LinearizeMonoidal.ε_toLinearMap, linearizeTrivialIso_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_bijective 📖	mathematical	—	Function.Bijective DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	Equiv.bijective inv_self_apply self_inv_apply
apply_eq_of_coe_eq 📖	mathematical	—	DFunLike.coe Representation DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	LinearMap.ext apply_bijective MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass inv_mul_cancel map_one MonoidHomClass.toOneHomClass QuotientGroup.eq isTrivial_def
apply_eq_of_leftRegular_eq_of_generator 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.zpowers DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring leftRegular	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike	—	Int.induction_on zpow_zero ofMulAction_apply inv_mul_cancel Finsupp.ext_iff zpow_add_one zpow_natCast pow_mul_comm' pow_succ' inv_mul_cancel_left zpow_sub zpow_neg zpow_one
apply_sub_id_partialSum_eq 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.instSub Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.id Fin.partialSum SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toPow SubNegMonoid.toSub	—	zero_add List.ofFn_congr pow_zero map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass add_zero pow_one map_pow Fin.partialSum_succ Fin.partialSum_init map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass pow_succ' map_mul MonoidHomClass.toMulHomClass sub_add_sub_cancel'
asAlgebraHom_def 📖	mathematical	—	asAlgebraHom DFunLike.coe Equiv MonoidHom LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring AlgHom MonoidAlgebra MonoidAlgebra.semiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike Equiv.instEquivLike MonoidAlgebra.lift	—	smulCommClass_self IsScalarTower.left
asAlgebraHom_of 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring Module.End MonoidAlgebra.semiring Module.End.instSemiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike asAlgebraHom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidAlgebra.nonAssocSemiring MonoidHom.instFunLike MonoidAlgebra.of Representation LinearMap RingHom.id Semiring.toNonAssocSemiring	—	smulCommClass_self IsScalarTower.left asAlgebraHom_single one_smul
asAlgebraHom_single 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring Module.End MonoidAlgebra.semiring Module.End.instSemiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike asAlgebraHom MonoidAlgebra.single LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instSMul DistribMulAction.toDistribSMul Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass	—	smulCommClass_self IsScalarTower.left MonoidAlgebra.lift_single
asAlgebraHom_single_one 📖	mathematical	—	DFunLike.coe AlgHom MonoidAlgebra CommSemiring.toSemiring Module.End MonoidAlgebra.semiring Module.End.instSemiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike asAlgebraHom MonoidAlgebra.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Representation LinearMap RingHom.id MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass	—	smulCommClass_self IsScalarTower.left asAlgebraHom_single one_smul
asGroupHom_apply 📖	mathematical	—	Units.val LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid DFunLike.coe MonoidHom Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instMulOneClass MonoidHom.instFunLike asGroupHom Representation MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—
asModuleEquiv_map_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids asModule instAddCommMonoidAsModule instModuleAsModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv asModuleEquiv MonoidAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction instModuleMonoidAlgebraAsModule Module.End LinearMap.instFunLike AlgHom Module.End.instSemiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Algebra.toSMul IsScalarTower.left AlgHom.funLike asAlgebraHom	—	RingHomInvPair.ids
asModuleEquiv_symm_map_rho 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids asModule instAddCommMonoidAsModule instModuleAsModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm asModuleEquiv LinearMap LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction instModuleMonoidAlgebraAsModule MonoidHom MonoidAlgebra.nonAssocSemiring MonoidAlgebra.of	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq smulCommClass_self IsScalarTower.left asAlgebraHom_single one_smul LinearEquiv.apply_symm_apply
asModuleEquiv_symm_map_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids asModule instAddCommMonoidAsModule instModuleAsModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm asModuleEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MonoidAlgebra MonoidAlgebra.semiring instModuleMonoidAlgebraAsModule RingHom RingHom.instFunLike algebraMap MonoidAlgebra.algebra Algebra.id	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq smulCommClass_self IsScalarTower.left asAlgebraHom_single map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass LinearEquiv.apply_symm_apply
directSum_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring DirectSum instAddCommMonoidDirectSum DirectSum.instModule MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike directSum DirectSum.lmap Representation	—	—
dualTensorHom_comm 📖	mathematical	—	LinearMap.comp TensorProduct Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap TensorProduct.addCommMonoid TensorProduct.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids dualTensorHom TensorProduct.map DFunLike.coe Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring dual linHom	—	TensorProduct.AlgebraTensorModule.curry_injective Algebra.to_smulCommClass LinearMap.instIsScalarTower IsScalarTower.right smulCommClass_self IsScalarTower.left RingHomCompTriple.ids LinearMap.ext IsScalarTower.to_smulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
dual_apply 📖	mathematical	—	DFunLike.coe Representation Module.Dual CommSemiring.toSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring dual smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike Module.Dual.transpose InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Algebra.to_smulCommClass
finsupp_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike finsupp LinearEquiv Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Finsupp.lsum LinearMap.comp Finsupp.lsingle Representation	—	—
finsupp_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring finsupp Finsupp.single	—	Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.single_zero
free_asModule_free 📖	mathematical	—	Module.Free MonoidAlgebra CommSemiring.toSemiring asModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instZero Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule free MonoidAlgebra.semiring instAddCommMonoidAsModule instModuleMonoidAlgebraAsModule	—	Module.Free.of_basis
free_single_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instZero Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring free Finsupp.single MulOne.toMul	—	finsupp_single ofMulAction_single
instFiniteAsModule 📖	mathematical	—	Module.Finite asModule instAddCommMonoidAsModule instModuleAsModule	—	Module.Finite.equiv RingHomInvPair.ids
instIsScalarTowerMonoidAlgebraAsModule 📖	mathematical	—	IsScalarTower MonoidAlgebra CommSemiring.toSemiring asModule Algebra.toSMul MonoidAlgebra.semiring MonoidAlgebra.algebra Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidAsModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModuleMonoidAlgebraAsModule instModuleAsModule	—	MonoidAlgebra.induction_on RingHomInvPair.ids MonoidAlgebra.smul_single mul_one single_smul one_smul smul_add add_smul smul_assoc MonoidAlgebra.isScalarTower IsScalarTower.right smul_eq_mul IsScalarTower.left
instIsTrivialTrivial 📖	mathematical	—	IsTrivial trivial	—	—
inv_self_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass inv_mul_cancel map_one MonoidHomClass.toOneHomClass
isTrivial_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	isTrivial_def
isTrivial_def 📖	mathematical	—	DFunLike.coe Representation LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.id	—	IsTrivial.out
ker_leftRegular_norm_eq 📖	mathematical	—	LinearMap.ker Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id norm leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.linearCombination AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submodule.ext leftRegular_norm_eq_zero_iff
leftRegular_norm_apply 📖	mathematical	—	norm Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap.comp RingHom.id RingHomCompTriple.ids DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip LinearMap.lsmul Module.End Finsupp.single InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp.linearCombination	—	Finsupp.lhom_ext' RingHomCompTriple.ids SMulCommClass.symm smulCommClass_self LinearMap.ext_ring LinearMap.coe_sum Finset.sum_apply Finset.sum_congr ofMulAction_single LinearMap.comp.congr_simp mul_one map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.linearCombination_single one_smul Finset.sum_bijective Group.mulRight_bijective
leftRegular_norm_eq_zero_iff 📖	mathematical	—	DFunLike.coe Module.End Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike RingHom.id norm leftRegular DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.instZero LinearMap Finsupp.linearCombination AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomCompTriple.ids SMulCommClass.symm smulCommClass_self leftRegular_norm_apply LinearMap.comp.congr_simp LinearMap.coe_sum Finset.sum_apply Finset.sum_congr ofMulAction_single mul_one map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.smul_single Finsupp.coe_finset_sum Finsupp.univ_sum_single_apply' Finsupp.ext_iff Finsupp.ext map_zero AddMonoidHomClass.toZeroHomClass
linHom_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring linHom LinearMap.comp RingHomCompTriple.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smulCommClass_self
norm_comp_self 📖	mathematical	—	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids norm DFunLike.coe Representation DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	LinearMap.ext RingHomCompTriple.ids LinearMap.coe_sum Finset.sum_apply Fintype.sum_bijective Group.mulRight_bijective map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
norm_ofDistribMulAction_eq 📖	mathematical	—	DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring norm ofDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	LinearMap.coe_sum Finset.sum_apply Finset.sum_congr
norm_ofMulDistribMulAction_eq 📖	mathematical	—	DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.toMul Module.End Int.instSemiring Additive.addCommMonoid CommGroup.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring norm ofMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid Finset.prod Finset.univ SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup	—	LinearMap.coe_sum Finset.sum_apply Finset.sum_congr Finset.prod_congr
norm_self_apply 📖	mathematical	—	DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring norm LinearMap Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	RingHomCompTriple.ids LinearMap.ext_iff norm_comp_self
ofDistribMulAction_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofDistribMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
ofModule_asAlgebraHom_apply_apply 📖	mathematical	—	DFunLike.coe Module.End RestrictScalars MonoidAlgebra CommSemiring.toSemiring instAddCommMonoidRestrictScalars RestrictScalars.module MonoidAlgebra.semiring MonoidAlgebra.algebra Algebra.id LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring AlgHom Module.End.instSemiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike asAlgebraHom ofModule AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm RestrictScalars.addEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	MonoidAlgebra.induction_on smulCommClass_self IsScalarTower.left asAlgebraHom_single one_smul map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass add_smul AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass RestrictScalars.addEquiv_symm_map_smul_smul
ofModule_asModule_act 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RestrictScalars MonoidAlgebra asModule instAddCommMonoidRestrictScalars instAddCommMonoidAsModule RestrictScalars.module MonoidAlgebra.semiring MonoidAlgebra.algebra Algebra.id instModuleMonoidAlgebraAsModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofModule AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm RestrictScalars.addEquiv LinearEquiv RingHomInvPair.ids instModuleAsModule DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm asModuleEquiv	—	RingHomInvPair.ids asModuleEquiv_symm_map_rho LinearEquiv.symm_apply_apply
ofMulActionSelfAsModuleEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv MonoidAlgebra CommSemiring.toSemiring MonoidAlgebra.semiring DivInvMonoid.toMonoid Group.toDivInvMonoid RingHom.id MonoidAlgebra.nonAssocSemiring Monoid.toMulOneClass Semiring.toNonAssocSemiring RingHomInvPair.ids asModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule ofMulAction Monoid.toMulAction instAddCommMonoidAsModule MonoidAlgebra.addCommMonoid instModuleMonoidAlgebraAsModule EquivLike.toFunLike LinearEquiv.instEquivLike ofMulActionSelfAsModuleEquiv Equiv.toFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearEquiv.toAddEquiv instModuleAsModule asModuleEquiv	—	RingHomInvPair.ids
ofMulActionSelfAsModuleEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv MonoidAlgebra CommSemiring.toSemiring MonoidAlgebra.semiring DivInvMonoid.toMonoid Group.toDivInvMonoid RingHom.id Semiring.toNonAssocSemiring MonoidAlgebra.nonAssocSemiring Monoid.toMulOneClass RingHomInvPair.ids asModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule ofMulAction Monoid.toMulAction MonoidAlgebra.addCommMonoid instAddCommMonoidAsModule instModuleMonoidAlgebraAsModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm ofMulActionSelfAsModuleEquiv Equiv.invFun AddEquiv.toEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearEquiv.toAddEquiv instModuleAsModule asModuleEquiv	—	RingHomInvPair.ids
ofMulAction_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofMulAction SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_inv_smul Finsupp.mapDomain_apply
ofMulAction_def 📖	mathematical	—	DFunLike.coe Representation Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap RingHom.id MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofMulAction Finsupp.lmapDomain SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—
ofMulAction_self_smul_eq_mul 📖	mathematical	—	MonoidAlgebra CommSemiring.toSemiring asModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule ofMulAction Monoid.toMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidAsModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction instModuleMonoidAlgebraAsModule instHMulMonoidAlgebraAsModuleFinsuppOfMulAction	—	MonoidAlgebra.induction_on Finsupp.ext smulCommClass_self IsScalarTower.left asAlgebraHom_single one_smul Finsupp.smulCommClass Algebra.to_smulCommClass ofMulAction_apply MonoidAlgebra.single_mul_apply one_mul add_smul add_mul Distrib.rightDistribClass smul_assoc instIsScalarTowerMonoidAlgebraAsModule Algebra.smul_mul_assoc
ofMulAction_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofMulAction Finsupp.single SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	Finsupp.mapDomain_single
ofMulDistribMulAction_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring Additive Additive.addCommMonoid CommGroup.toCommMonoid AddCommGroup.toIntModule Additive.addCommGroup LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofMulDistribMulAction Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Additive.toMul	—	—
ofQuotient_coe_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ofQuotient	—	—
prod_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid Prod.instModule LinearMap.instFunLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike prod Representation	—	—
quotient_apply 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	DFunLike.coe MonoidHom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike quotient Submodule.mapQ Representation	—	—
self_comp_norm 📖	mathematical	—	LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe Representation DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring norm	—	LinearMap.ext RingHomCompTriple.ids LinearMap.coe_sum Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Fintype.sum_bijective Group.mulLeft_bijective map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
self_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_inv_cancel map_one MonoidHomClass.toOneHomClass
self_norm_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Module.End norm	—	RingHomCompTriple.ids LinearMap.ext_iff self_comp_norm
single_smul 📖	mathematical	—	MonoidAlgebra CommSemiring.toSemiring asModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidAsModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction instModuleMonoidAlgebraAsModule MonoidAlgebra.single DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearEquiv RingHomInvPair.ids instModuleAsModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv asModuleEquiv	—	RingHomInvPair.ids smulCommClass_self LinearMap.smul_apply IsScalarTower.left asAlgebraHom_single asModuleEquiv_map_smul
smul_ofModule_asModule 📖	mathematical	—	DFunLike.coe AddEquiv RestrictScalars MonoidAlgebra CommSemiring.toSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidRestrictScalars EquivLike.toFunLike AddEquiv.instEquivLike RestrictScalars.addEquiv LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids asModule RestrictScalars.module MonoidAlgebra.semiring MonoidAlgebra.algebra Algebra.id ofModule instAddCommMonoidAsModule instModuleAsModule DFinsupp.instEquivLikeLinearEquiv asModuleEquiv SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModuleMonoidAlgebraAsModule	—	RingHomInvPair.ids smulCommClass_self IsScalarTower.left ofModule_asAlgebraHom_apply_apply AddEquiv.apply_symm_apply
smul_one_tprod_asModule 📖	mathematical	—	MonoidAlgebra CommSemiring.toSemiring asModule TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule tprod Representation instOneMonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidAsModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction instModuleMonoidAlgebraAsModule TensorProduct.tmul	—	smulCommClass_self IsScalarTower.left MonoidAlgebra.lift_apply LinearMap.finsupp_sum_apply Finset.sum_congr TensorProduct.tmul_sum TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower
smul_tprod_one_asModule 📖	mathematical	—	MonoidAlgebra CommSemiring.toSemiring asModule TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule tprod Representation instOneMonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidAsModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidAlgebra.semiring Module.toDistribMulAction instModuleMonoidAlgebraAsModule TensorProduct.tmul	—	smulCommClass_self IsScalarTower.left MonoidAlgebra.lift_apply LinearMap.finsupp_sum_apply Finset.sum_congr TensorProduct.sum_tmul
subrepresentation_apply 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring DFunLike.coe Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	DFunLike.coe MonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike subrepresentation LinearMap.restrict Representation	—	—
tprod_apply 📖	mathematical	—	DFunLike.coe Representation TensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring tprod TensorProduct.map	—	—
trivial_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring trivial	—	—

Representation.IsTrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	DFunLike.coe Representation LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.id	—	—

---

← Back to Index