Documentation Verification Report

Module

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

Statistics

Metric	Count
Definitions `basis`, `distribMulAction`, `lsingle`, `singleDistribMulActionHom`, `basis`, `comapDistribMulActionSelf`, `distribMulAction`, `lsingle`, `singleDistribMulActionHom`, `submoduleOfSMulMem`	10
Theorems `basis_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`, `of'_mem_span`, `smulCommClass_self`, `smulCommClass_symm_self`, `basis_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`, `of_mem_span_of_iff`, `smulCommClass_self`, `smulCommClass_symm_self`, `smul_of`	29
Total	39

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	1 math math: `basis_apply`
`distribMulAction` 📖	CompOp	5 math math: `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`

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`	—	—
`distribMulActionHom_ext'` 📖	—	`DistribMulActionHom.comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `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` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `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`	—	`Finsupp.faithfulSMul`
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `AddMonoidAlgebra` `addAddCommMonoid` `module`	—	`Finsupp.moduleIsTorsionFree`
`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` `AddSubmonoid.instSetLike` `AddSubmonoid.closure`	—	`MonoidHom.instMonoidHomClass` `MonoidHom.map_mclosure` `of'_mem_span` `Set.image_congr'` `of'_eq_of`
`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`

MonoidAlgebra

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	1 math math: `basis_apply`
`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	—

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`	—	—
`distribMulActionHom_ext'` 📖	—	`DistribMulActionHom.comp` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `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` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MonoidAlgebra` `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`	—	`Finsupp.faithfulSMul`
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `MonoidAlgebra` `addCommMonoid` `module`	—	`Finsupp.moduleIsTorsionFree`
`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` 📖	—	`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`	—	—	`of_mem_span_of_iff` `MonoidHom.instMonoidHomClass` `MonoidHom.map_mclosure`
`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`

---

← Back to Index