Module

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

Statistics

Metric	Count
Definitions `basis`, `coeffLinearEquiv`, `distribMulAction`, `lsingle`, `singleDistribMulActionHom`, `supported`, `supportedEquivFinsupp`, `basis`, `coeffLinearEquiv`, `comapDistribMulActionSelf`, `distribMulAction`, `lsingle`, `singleDistribMulActionHom`, `submoduleOfSMulMem`, `supported`, `supportedEquivFinsupp`	16
Theorems `basis_apply`, `coeffLinearEquiv_apply`, `coeffLinearEquiv_symm_apply`, `distribMulActionHom_ext'`, `distribMulActionHom_ext'_iff`, `faithfulSMul`, `instIsTorsionFree`, `isScalarTower_self`, `lhom_ext'`, `lhom_ext'_iff`, `liftNC_smul`, `lsingle_apply`, `mem_closure_of_mem_span_closure`, `mem_supported`, `mem_supported'`, `of'_mem_span`, `smulCommClass_self`, `smulCommClass_symm_self`, `supportedEquivFinsupp_apply_apply`, `supportedEquivFinsupp_apply_support_val`, `supportedEquivFinsupp_symm_apply_coe_apply`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `supported_eq_map`, `supported_eq_span_single`, `supported_mono`, `basis_apply`, `coeffLinearEquiv_apply`, `coeffLinearEquiv_symm_apply`, `distribMulActionHom_ext'`, `distribMulActionHom_ext'_iff`, `faithfulSMul`, `instIsTorsionFree`, `isScalarTower_self`, `lhom_ext'`, `lhom_ext'_iff`, `liftNC_smul`, `lsingle_apply`, `mem_closure_of_mem_span_closure`, `mem_supported`, `mem_supported'`, `of_mem_span_of_iff`, `smulCommClass_self`, `smulCommClass_symm_self`, `smul_of`, `supportedEquivFinsupp_apply_apply`, `supportedEquivFinsupp_apply_support_val`, `supportedEquivFinsupp_symm_apply_coe_apply`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `supported_eq_map`, `supported_eq_span_single`, `supported_mono`	51
Total	67

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	1 math math: `basis_apply`
`coeffLinearEquiv` 📖	CompOp	3 math math: `coeffLinearEquiv_apply`, `supported_eq_map`, `coeffLinearEquiv_symm_apply`
`distribMulAction` 📖	CompOp	6 math math: `MvPolynomial.universalFactorizationMap_comp_map`, `mapDomainNonUnitalAlgHom_apply`, `nonUnitalAlgHom_ext'_iff`, `liftMagma_apply_apply`, `liftMagma_symm_apply`, `distribMulActionHom_ext'_iff`
`lsingle` 📖	CompOp	6 math math: `domCongr_comp_lsingle`, `comul_single`, `lsingle_apply`, `LaurentPolynomial.comul_C`, `lhom_ext'_iff`, `LaurentPolynomial.comul_C_mul_T`
`singleDistribMulActionHom` 📖	CompOp	1 math math: `distribMulActionHom_ext'_iff`
`supported` 📖	CompOp	9 math math: `supportedEquivFinsupp_apply_apply`, `supportedEquivFinsupp_apply_support_val`, `supported_eq_span_single`, `supported_eq_map`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `supported_mono`, `supportedEquivFinsupp_symm_apply_coe_apply`, `mem_supported'`, `mem_supported`
`supportedEquivFinsupp` 📖	CompOp	4 math math: `supportedEquivFinsupp_apply_apply`, `supportedEquivFinsupp_apply_support_val`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `supportedEquivFinsupp_symm_apply_coe_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `AddMonoidAlgebra` `addAddCommMonoid` `module` `Semiring.toModule` `Module.Basis.instFunLike` `basis` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`coeffLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddMonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `coeffLinearEquiv` `coeff`	—	`RingHomInvPair.ids`
`coeffLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidAlgebra` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `addAddCommMonoid` `Finsupp.module` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `coeffLinearEquiv` `ofCoeff`	—	`RingHomInvPair.ids`
`distribMulActionHom_ext'` 📖	—	`DistribMulActionHom.comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidAlgebra` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `distribMulAction` `singleDistribMulActionHom` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	—	`MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `Finsupp.distribMulActionHom_ext'`
`distribMulActionHom_ext'_iff` 📖	mathematical	—	`DistribMulActionHom.comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidAlgebra` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `distribMulAction` `singleDistribMulActionHom` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	`MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `distribMulActionHom_ext'`
`faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass`	—	—
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `AddMonoidAlgebra` `addAddCommMonoid` `module`	—	—
`isScalarTower_self` 📖	mathematical	—	`IsScalarTower` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `nonUnitalNonAssocSemiring`	—	`ext` `mul_apply` `Finsupp.sum_smul_index'` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `smul_mul_assoc` `Finsupp.smul_sum` `smul_ite` `smul_zero`
`lhom_ext'` 📖	—	`LinearMap.comp` `AddMonoidAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addAddCommMonoid` `module` `RingHom.id` `RingHomCompTriple.ids` `lsingle`	—	—	`RingHomCompTriple.ids` `Finsupp.lhom_ext'`
`lhom_ext'_iff` 📖	mathematical	—	`LinearMap.comp` `AddMonoidAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addAddCommMonoid` `module` `RingHom.id` `RingHomCompTriple.ids` `lsingle`	—	`RingHomCompTriple.ids` `lhom_ext'`
`liftNC_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `instDistribSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `addHom_ext'` `AddMonoidHom.ext` `smul_single'` `liftNC_single` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc` `DFunLike.congr_fun`
`lsingle_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addAddCommMonoid` `module` `LinearMap.instFunLike` `lsingle` `single`	—	—
`mem_closure_of_mem_span_closure` 📖	mathematical	`AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `Submonoid.instSetLike` `Submonoid.closure` `Set.image` `of'`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	—	`MonoidHom.instMonoidHomClass` `MonoidHom.map_mclosure` `of'_mem_span` `Set.image_congr'` `of'_eq_of`
`mem_supported` 📖	mathematical	—	`AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff`	—	—
`mem_supported'` 📖	mathematical	—	`AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `coeff`	—	`mem_supported` `SetLike.mem_coe` `Finsupp.mem_support_iff` `not_imp_comm`
`of'_mem_span` 📖	mathematical	—	`AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `of'` `Set` `Set.instMembership`	—	`Finsupp.single_mem_span_single`
`smulCommClass_self` 📖	mathematical	—	`SMulCommClass` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `nonUnitalNonAssocSemiring`	—	`ext` `mul_apply` `Finsupp.coe_smul` `Finsupp.sum_smul_index'` `MulZeroClass.mul_zero` `Finset.sum_congr` `mul_smul_comm` `Finset.smul_sum` `smul_ite` `smul_zero`
`smulCommClass_symm_self` 📖	mathematical	—	`SMulCommClass` `AddMonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `nonUnitalNonAssocSemiring` `smulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`SMulCommClass.symm` `smulCommClass_self`
`supportedEquivFinsupp_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `supportedEquivFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `coeff` `Set` `Set.instMembership`	—	`RingHomInvPair.ids`
`supportedEquivFinsupp_apply_support_val` 📖	mathematical	—	`Finset.val` `Set` `Set.instMembership` `Finsupp.support` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `Finsupp` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `supportedEquivFinsupp` `Multiset.map` `Finset` `Finset.instSetLike` `Finset.filter` `Classical.decPred` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `coeff` `Set.instHasSubset` `SetLike.coe` `LinearMap` `Finsupp.supported` `LinearMap.instFunLike` `LinearEquiv.toLinearMap` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ofCoeff` `Multiset.attach` `Multiset.filter`	—	`RingHomInvPair.ids`
`supportedEquivFinsupp_symm_apply_coe_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Set.Elem` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `supportedEquivFinsupp` `Set` `Set.instMembership` `Classical.decPred` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`supportedEquivFinsupp_symm_apply_coe_support_val` 📖	mathematical	—	`Finset.val` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `Submodule` `addAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp` `Set.Elem` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `supportedEquivFinsupp` `Multiset.map` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Multiset.add_zero`
`supported_eq_map` 📖	mathematical	—	`supported` `Submodule.map` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `addAddCommMonoid` `Finsupp.module` `module` `RingHom.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `coeffLinearEquiv` `Finsupp.supported`	—	`Submodule.comap_equiv_eq_map_symm` `RingHomInvPair.ids`
`supported_eq_span_single` 📖	mathematical	—	`supported` `Semiring.toModule` `Submodule.span` `AddMonoidAlgebra` `addAddCommMonoid` `module` `Set.image` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `supported_eq_map` `Submodule.map.congr_simp` `Finsupp.supported_eq_span_single` `Submodule.map_span` `Set.image_congr` `Set.image_comp`
`supported_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Submodule` `AddMonoidAlgebra` `addAddCommMonoid` `module` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `supported`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `RingHomInvPair.ids`

MonoidAlgebra

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	1 math math: `basis_apply`
`coeffLinearEquiv` 📖	CompOp	3 math math: `coeffLinearEquiv_symm_apply`, `coeffLinearEquiv_apply`, `supported_eq_map`
`comapDistribMulActionSelf` 📖	CompOp	—
`distribMulAction` 📖	CompOp	15 math math: `liftMagma_apply_apply`, `FreeNonUnitalNonAssocAlgebra.of_comp_lift`, `FreeNonUnitalNonAssocAlgebra.lift_unique`, `distribMulActionHom_ext'_iff`, `FreeLieAlgebra.liftAux_map_smul`, `FreeLieAlgebra.liftAux_map_add`, `FreeNonUnitalNonAssocAlgebra.lift_symm_apply`, `FreeLieAlgebra.liftAux_map_mul`, `FreeLieAlgebra.liftAux_spec`, `nonUnitalAlgHom_ext'_iff`, `liftMagma_symm_apply`, `mapDomainNonUnitalAlgHom_apply`, `FreeNonUnitalNonAssocAlgebra.lift_of_apply`, `FreeNonUnitalNonAssocAlgebra.hom_ext_iff`, `FreeNonUnitalNonAssocAlgebra.lift_comp_of`
`lsingle` 📖	CompOp	4 math math: `lsingle_apply`, `domCongr_comp_lsingle`, `lhom_ext'_iff`, `comul_single`
`singleDistribMulActionHom` 📖	CompOp	1 math math: `distribMulActionHom_ext'_iff`
`submoduleOfSMulMem` 📖	CompOp	—
`supported` 📖	CompOp	9 math math: `supportedEquivFinsupp_symm_apply_coe_apply`, `supported_eq_span_single`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `supportedEquivFinsupp_apply_support_val`, `supportedEquivFinsupp_apply_apply`, `supported_eq_map`, `mem_supported`, `supported_mono`, `mem_supported'`
`supportedEquivFinsupp` 📖	CompOp	4 math math: `supportedEquivFinsupp_symm_apply_coe_apply`, `supportedEquivFinsupp_symm_apply_coe_support_val`, `supportedEquivFinsupp_apply_support_val`, `supportedEquivFinsupp_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `MonoidAlgebra` `addCommMonoid` `module` `Semiring.toModule` `Module.Basis.instFunLike` `basis` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	—
`coeffLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MonoidAlgebra` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `coeffLinearEquiv` `coeff`	—	`RingHomInvPair.ids`
`coeffLinearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MonoidAlgebra` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `addCommMonoid` `Finsupp.module` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `coeffLinearEquiv` `ofCoeff`	—	`RingHomInvPair.ids`
`distribMulActionHom_ext'` 📖	—	`DistribMulActionHom.comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidAlgebra` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addCommMonoid` `distribMulAction` `singleDistribMulActionHom` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	—	`MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `Finsupp.distribMulActionHom_ext'`
`distribMulActionHom_ext'_iff` 📖	mathematical	—	`DistribMulActionHom.comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidAlgebra` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `addCommMonoid` `distribMulAction` `singleDistribMulActionHom` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	`MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `distribMulActionHom_ext'`
`faithfulSMul` 📖	mathematical	—	`FaithfulSMul` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass`	—	—
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `MonoidAlgebra` `addCommMonoid` `module`	—	—
`isScalarTower_self` 📖	mathematical	—	`IsScalarTower` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `nonUnitalNonAssocSemiring`	—	`ext` `mul_apply` `Finsupp.sum_smul_index'` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `smul_mul_assoc` `Finsupp.smul_sum` `smul_ite` `smul_zero`
`lhom_ext'` 📖	—	`LinearMap.comp` `MonoidAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `RingHom.id` `RingHomCompTriple.ids` `lsingle`	—	—	`RingHomCompTriple.ids` `Finsupp.lhom_ext'`
`lhom_ext'_iff` 📖	mathematical	—	`LinearMap.comp` `MonoidAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `RingHom.id` `RingHomCompTriple.ids` `lsingle`	—	`RingHomCompTriple.ids` `lhom_ext'`
`liftNC_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `instDistribSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `addHom_ext'` `AddMonoidHom.ext` `smul_single'` `liftNC_single` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc` `DFunLike.congr_fun`
`lsingle_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `lsingle` `single`	—	—
`mem_closure_of_mem_span_closure` 📖	mathematical	`MonoidAlgebra` `Submodule` `addCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `Submonoid.instSetLike` `Submonoid.closure` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `of`	`Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.closure`	—	`of_mem_span_of_iff` `MonoidHom.instMonoidHomClass` `MonoidHom.map_mclosure`
`mem_supported` 📖	mathematical	—	`MonoidAlgebra` `Submodule` `addCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff`	—	—
`mem_supported'` 📖	mathematical	—	`MonoidAlgebra` `Submodule` `addCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `coeff`	—	—
`of_mem_span_of_iff` 📖	mathematical	—	`MonoidAlgebra` `Submodule` `addCommMonoid` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `Set` `Set.instMembership`	—	`Finsupp.single_mem_span_single`
`smulCommClass_self` 📖	mathematical	—	`SMulCommClass` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `nonUnitalNonAssocSemiring`	—	`ext` `mul_apply` `Finsupp.coe_smul` `Finsupp.sum_smul_index'` `MulZeroClass.mul_zero` `Finset.sum_congr` `mul_smul_comm` `Finset.smul_sum` `smul_ite` `smul_zero`
`smulCommClass_symm_self` 📖	mathematical	—	`SMulCommClass` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `nonUnitalNonAssocSemiring` `smulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`SMulCommClass.symm` `smulCommClass_self`
`smul_of` 📖	mathematical	—	`MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `nonAssocSemiring` `MonoidHom.instFunLike` `of` `single`	—	`smul_single` `mul_one`
`supportedEquivFinsupp_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `MonoidAlgebra` `Submodule` `addCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `supportedEquivFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `coeff` `Set` `Set.instMembership`	—	`RingHomInvPair.ids`
`supportedEquivFinsupp_apply_support_val` 📖	mathematical	—	`Finset.val` `Set` `Set.instMembership` `Finsupp.support` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `MonoidAlgebra` `Submodule` `addCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `Finsupp` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `supportedEquivFinsupp` `Multiset.map` `Finset` `Finset.instSetLike` `Finset.filter` `Classical.decPred` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `coeff` `Set.instHasSubset` `SetLike.coe` `LinearMap` `Finsupp.supported` `LinearMap.instFunLike` `LinearEquiv.toLinearMap` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ofCoeff` `Multiset.attach` `Multiset.filter`	—	`RingHomInvPair.ids`
`supportedEquivFinsupp_symm_apply_coe_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `MonoidAlgebra` `Submodule` `addCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Set.Elem` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `supportedEquivFinsupp` `Set` `Set.instMembership` `Classical.decPred` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`supportedEquivFinsupp_symm_apply_coe_support_val` 📖	mathematical	—	`Finset.val` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `Submodule` `addCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `supported` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp` `Set.Elem` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `supportedEquivFinsupp` `Multiset.map` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Multiset.add_zero`
`supported_eq_map` 📖	mathematical	—	`supported` `Submodule.map` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `addCommMonoid` `Finsupp.module` `module` `RingHom.id` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `coeffLinearEquiv` `Finsupp.supported`	—	`Submodule.comap_equiv_eq_map_symm` `RingHomInvPair.ids`
`supported_eq_span_single` 📖	mathematical	—	`supported` `Semiring.toModule` `Submodule.span` `MonoidAlgebra` `addCommMonoid` `module` `Set.image` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `supported_eq_map` `Submodule.map.congr_simp` `Finsupp.supported_eq_span_single` `Submodule.map_span` `Set.image_congr`
`supported_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Submodule` `MonoidAlgebra` `addCommMonoid` `module` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `supported`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `RingHomInvPair.ids`

---

← Back to Index