Documentation Verification Report

Internal

📁 Source: Mathlib/Algebra/DirectSum/Internal.lean

Statistics

Metric	Count
Definitions `coeAlgHom`, `coeRingHom`, `instAlgebra`, `instAlgebraSubtypeMemOfNat`, `instCommRing`, `instCommSemiring`, `instRing`, `instSemiring`, `subalgebra`, `subring`, `subsemiring`, `gcommRing`, `gcommSemiring`, `gnonUnitalNonAssocSemiring`, `gring`, `gsemiring`, `galgebra`	17
Theorems `coeAlgHom_of`, `coeRingHom_of`, `coe_mul_apply`, `coe_mul_apply_eq_dfinsuppSum`, `coe_mul_apply_eq_sum_antidiagonal`, `coe_mul_of_apply`, `coe_mul_of_apply_add`, `coe_mul_of_apply_aux`, `coe_mul_of_apply_of_le`, `coe_mul_of_apply_of_mem_zero`, `coe_mul_of_apply_of_not_le`, `coe_of_mul_apply`, `coe_of_mul_apply_add`, `coe_of_mul_apply_aux`, `coe_of_mul_apply_of_le`, `coe_of_mul_apply_of_mem_zero`, `coe_of_mul_apply_of_not_le`, `algebraMap_apply`, `coe_algebraMap`, `coe_intCast`, `coe_natCast`, `coe_ofNat`, `smul`, `algebraMap_mem_graded`, `homogeneous_zero_submodule`, `intCast_mem_graded`, `natCast_mem_graded`, `iSup_eq_toSubmodule_range`, `nat_power_gradedMonoid`, `coe_galgebra_toFun`, `finsetProd_apply_eq_zero`, `finsetProd_apply_eq_zero'`, `listProd_apply_eq_zero`, `listProd_apply_eq_zero'`, `mul_apply_eq_zero`, `multisetProd_apply_eq_zero`, `multisetProd_apply_eq_zero'`	37
Total	54

DirectSum

Definitions

Name	Category	Theorems
`coeAlgHom` 📖	CompOp	2 math math: `coeAlgHom_of`, `Submodule.iSup_eq_toSubmodule_range`
`coeRingHom` 📖	CompOp	1 math math: `coeRingHom_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeAlgHom_of` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `DirectSum` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `semiring` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `instAlgebra` `Submodule.module` `Submodule.galgebra` `AlgHom.funLike` `coeAlgHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`toSemiring_of`
`coeRingHom_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `DirectSum` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.gsemiring` `RingHom.instFunLike` `coeRingHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`toSemiring_of`
`coe_mul_apply` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Finset.sum` `Finset.filter` `SProd.sprod` `Finset` `Finset.instSProd` `DFinsupp.support` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `mul_eq_sum_support_ghas_mul` `DFinsupp.finset_sum_apply` `AddSubmonoidClass.coe_finset_sum` `Finset.sum_congr` `coe_of_apply`
`coe_mul_apply_eq_dfinsuppSum` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFinsupp.sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `mul_eq_dfinsuppSum` `DFinsupp.sum_apply` `DFinsupp.sum.eq_1` `AddSubmonoidClass.coe_finset_sum` `of_eq_same` `of_eq_of_ne`
`coe_mul_apply_eq_sum_antidiagonal` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`SetLike.GradedMonoid.toGradedMul` `AddSubmonoidClass.toZeroMemClass` `coe_mul_apply` `Finset.sum_subset` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`coe_mul_of_apply` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`SetLike.GradedMonoid.toGradedMul` `coe_mul_of_apply_of_le` `coe_mul_of_apply_of_not_le`
`coe_mul_of_apply_add` 📖	mathematical	—	`SetLike.instMembership` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddRightCancelMonoid.toAddMonoid` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coe_mul_of_apply_aux` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd`
`coe_mul_of_apply_aux` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`SetLike.GradedMonoid.toGradedMul` `AddSubmonoidClass.toZeroMemClass` `coe_mul_apply_eq_dfinsuppSum` `DFinsupp.sum_comm` `DFinsupp.sum_single_index` `DFinsupp.sum.congr_simp` `MulZeroClass.mul_zero` `DFinsupp.sum_zero` `Finset.sum_congr` `Finset.sum_ite_eq'` `DFinsupp.notMem_support_iff` `ZeroMemClass.coe_zero` `MulZeroClass.zero_mul`
`coe_mul_of_apply_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coe_mul_of_apply_aux` `eq_tsub_iff_add_eq_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono`
`coe_mul_of_apply_of_mem_zero` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coe_mul_of_apply_aux` `add_zero`
`coe_mul_of_apply_of_not_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`SetLike.GradedMonoid.toGradedMul` `AddSubmonoidClass.toZeroMemClass` `coe_mul_apply_eq_dfinsuppSum` `DFinsupp.sum_comm` `DFinsupp.sum_single_index` `DFinsupp.sum.congr_simp` `MulZeroClass.mul_zero` `DFinsupp.sum_zero` `DFinsupp.sum.eq_1` `Finset.sum_ite_of_false` `LE.le.trans_eq` `self_le_add_left` `Finset.sum_const_zero`
`coe_of_mul_apply` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`SetLike.GradedMonoid.toGradedMul` `coe_of_mul_apply_of_le` `coe_of_mul_apply_of_not_le`
`coe_of_mul_apply_add` 📖	mathematical	—	`SetLike.instMembership` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddLeftCancelMonoid.toAddMonoid` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coe_of_mul_apply_aux` `add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`coe_of_mul_apply_aux` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`SetLike.GradedMonoid.toGradedMul` `AddSubmonoidClass.toZeroMemClass` `coe_mul_apply_eq_dfinsuppSum` `DFinsupp.sum_single_index` `DFinsupp.sum.congr_simp` `MulZeroClass.zero_mul` `DFinsupp.sum_zero` `Finset.sum_congr` `Finset.sum_ite_eq'` `DFinsupp.notMem_support_iff` `ZeroMemClass.coe_zero` `MulZeroClass.mul_zero`
`coe_of_mul_apply_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coe_of_mul_apply_aux` `eq_tsub_iff_add_eq_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono` `add_comm`
`coe_of_mul_apply_of_mem_zero` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coe_of_mul_apply_aux` `zero_add`
`coe_of_mul_apply_of_not_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidHom` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`SetLike.GradedMonoid.toGradedMul` `AddSubmonoidClass.toZeroMemClass` `coe_mul_apply_eq_dfinsuppSum` `DFinsupp.sum_single_index` `DFinsupp.sum.congr_simp` `MulZeroClass.zero_mul` `DFinsupp.sum_zero` `DFinsupp.sum.eq_1` `Finset.sum_ite_of_false` `LE.le.trans_eq` `self_le_add_right` `Finset.sum_const_zero`

SetLike

Definitions

Name	Category	Theorems
`gcommRing` 📖	CompOp	—
`gcommSemiring` 📖	CompOp	4 math math: `finsetProd_apply_eq_zero`, `multisetProd_apply_eq_zero'`, `multisetProd_apply_eq_zero`, `finsetProd_apply_eq_zero'`
`gnonUnitalNonAssocSemiring` 📖	CompOp	22 math math: `mul_apply_eq_zero`, `DirectSum.coe_of_mul_apply_aux`, `ExteriorAlgebra.GradedAlgebra.ι_sq_zero`, `DirectSum.coe_of_mul_apply_add`, `DirectSum.coe_mul_of_apply_of_not_le`, `DirectSum.coe_mul_apply`, `listProd_apply_eq_zero'`, `DirectSum.coe_of_mul_apply_of_not_le`, `DirectSum.coe_mul_of_apply_of_mem_zero`, `DirectSum.coe_mul_of_apply_aux`, `DirectSum.decompose_symm_mul`, `DirectSum.coe_mul_of_apply_add`, `DirectSum.coe_of_mul_apply_of_le`, `DirectSum.coe_mul_of_apply_of_le`, `DirectSum.coe_of_mul_apply_of_mem_zero`, `DirectSum.coe_mul_of_apply`, `DirectSum.coe_mul_apply_eq_dfinsuppSum`, `listProd_apply_eq_zero`, `DirectSum.coe_mul_apply_eq_sum_antidiagonal`, `DirectSum.decompose_mul`, `CliffordAlgebra.GradedAlgebra.ι_sq_scalar`, `DirectSum.coe_of_mul_apply`
`gring` 📖	CompOp	2 math math: `GradedTensorProduct.auxEquiv_mul`, `GradedTensorProduct.mulHom_apply`
`gsemiring` 📖	CompOp	16 math math: `ExteriorAlgebra.GradedAlgebra.liftι_eq`, `DirectSum.decomposeAlgEquiv_symm_apply`, `GradedTensorProduct.auxEquiv_one`, `AddMonoidAlgebra.decomposeAux_coe`, `GradedTensorProduct.auxEquiv_symm_one`, `Submodule.setLike.coe_galgebra_toFun`, `DirectSum.coeAlgHom_of`, `DirectSum.decompose_symm_algebraMap`, `DirectSum.decompose_algebraMap`, `DirectSum.coeRingHom_of`, `DirectSum.decomposeAlgEquiv_apply`, `Submodule.iSup_eq_toSubmodule_range`, `AddMonoidAlgebra.decomposeAux_single`, `AddMonoidAlgebra.decomposeAux_eq_decompose`, `CliffordAlgebra.GradedAlgebra.lift_ι_eq`, `CliffordAlgebra.GradedAlgebra.ι_sq_scalar`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_mem_graded` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instMembership` `Submodule.setLike` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one` `Submodule.smul_mem` `one_mem_graded`
`homogeneous_zero_submodule` 📖	mathematical	—	`IsHomogeneousElem` `Submodule` `Submodule.setLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Submodule.zero_mem`
`intCast_mem_graded` 📖	mathematical	—	`instMembership` `AddGroupWithOne.toIntCast`	—	`Int.cast_natCast` `natCast_mem_graded` `AddSubgroupClass.toAddSubmonoidClass` `Int.cast_negSucc` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass`
`natCast_mem_graded` 📖	mathematical	—	`instMembership` `AddMonoidWithOne.toNatCast`	—	`Nat.cast_zero` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Nat.cast_succ` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `one_mem_graded`

SetLike.GradeZero

Definitions

Name	Category	Theorems
`instAlgebra` 📖	CompOp	1 math math: `coe_algebraMap`
`instAlgebraSubtypeMemOfNat` 📖	CompOp	6 math math: `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero`, `AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc`, `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous`, `algebraMap_apply`, `HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization`, `AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero`
`instCommRing` 📖	CompOp	10 math math: `AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc`, `AlgebraicGeometry.Proj.valuativeCriterion_existence`, `AlgebraicGeometry.Proj.instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `AlgebraicGeometry.Proj.isSeparated`, `AlgebraicGeometry.Proj.awayι_toSpecZero`, `AlgebraicGeometry.Proj.awayι_toSpecZero_assoc`, `AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero`, `AlgebraicGeometry.Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `AlgebraicGeometry.Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`, `AlgebraicGeometry.Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat`
`instCommSemiring` 📖	CompOp	8 math math: `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero`, `GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous`, `algebraMap_apply`, `HomogeneousLocalization.awayMapₐ_apply`, `HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization`, `HomogeneousLocalization.algebraMap_eq`, `HomogeneousLocalization.Away.finiteType`, `AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective`
`instRing` 📖	CompOp	1 math math: `coe_intCast`
`instSemiring` 📖	CompOp	9 math math: `GradedRing.GradeZero.isNoetherianRing`, `GradedRing.projZeroRingHom'_apply_coe`, `HomogeneousLocalization.awayMap_fromZeroRingHom`, `HomogeneousLocalization.Away.span_mk_prod_pow_eq_top`, `coe_algebraMap`, `GradedRing.projZeroRingHom'_surjective`, `coe_natCast`, `AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective`, `GradedRing.coe_projZeroRingHom'_apply`
`subalgebra` 📖	CompOp	—
`subring` 📖	CompOp	—
`subsemiring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebraSubtypeMemOfNat`	—	—
`coe_algebraMap` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `RingHom` `instSemiring` `Submodule.addSubmonoidClass` `RingHom.instFunLike` `algebraMap` `instAlgebra`	—	`Submodule.addSubmonoidClass`
`coe_intCast` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `instRing`	—	—
`coe_natCast` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiring`	—	—
`coe_ofNat` 📖	mathematical	—	`SetLike.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

SetLike.Homogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	`SetLike.IsHomogeneousElem` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.setLike`	`Algebra.toSMul`	—	`Submodule.smul_mem`

Submodule

Definitions

Name	Category	Theorems
`galgebra` 📖	CompOp	15 math math: `ExteriorAlgebra.GradedAlgebra.liftι_eq`, `DirectSum.decomposeAlgEquiv_symm_apply`, `AddMonoidAlgebra.decomposeAux_coe`, `setLike.coe_galgebra_toFun`, `DirectSum.coeAlgHom_of`, `GradedTensorProduct.auxEquiv_mul`, `DirectSum.decompose_symm_algebraMap`, `DirectSum.decompose_algebraMap`, `GradedTensorProduct.mulHom_apply`, `DirectSum.decomposeAlgEquiv_apply`, `iSup_eq_toSubmodule_range`, `AddMonoidAlgebra.decomposeAux_single`, `AddMonoidAlgebra.decomposeAux_eq_decompose`, `CliffordAlgebra.GradedAlgebra.lift_ι_eq`, `CliffordAlgebra.GradedAlgebra.ι_sq_scalar`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_eq_toSubmodule_range` 📖	mathematical	—	`iSup` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `DFunLike.coe` `OrderEmbedding` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `AlgHom.range` `DirectSum` `SetLike.instMembership` `setLike` `addCommMonoid` `DirectSum.semiring` `SetLike.gsemiring` `addSubmonoidClass` `DirectSum.instAlgebra` `module` `galgebra` `DirectSum.coeAlgHom`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `AddMonoid.nat_smulCommClass'` `addSubmonoidClass` `iSup_eq_range_dfinsupp_lsum` `SetLike.coe_injective`
`nat_power_gradedMonoid` 📖	mathematical	—	`SetLike.GradedMonoid` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `setLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instAddMonoid` `instPowNat` `IsScalarTower.right`	—	`IsScalarTower.right` `one_le` `pow_zero` `le_refl` `pow_add` `mul_mem_mul`

Submodule.setLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_galgebra_toFun` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Submodule.addCommMonoid` `AddMonoidHom.instFunLike` `DirectSum.GAlgebra.toFun` `Submodule.module` `SetLike.gsemiring` `Submodule.addSubmonoidClass` `Submodule.galgebra` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Submodule.addSubmonoidClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsetProd_apply_eq_zero` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `Finset.card` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Finset.prod` `CommSemiring.toCommMonoid` `DirectSum.commSemiring` `SetLike.gcommSemiring`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `SetLike.GradedMonoid.toGradedOne` `Finset.prod_toList` `listProd_apply_eq_zero` `Finset.length_toList`
`finsetProd_apply_eq_zero'` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum`	`Finset.prod` `CommSemiring.toCommMonoid` `DirectSum.commSemiring` `SetLike.gcommSemiring`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `SetLike.GradedMonoid.toGradedOne` `Finset.prod_map_toList` `listProd_apply_eq_zero'` `Finset.sum_map_toList`
`listProd_apply_eq_zero` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`DirectSum.instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DirectSum.instOne` `SetLike.gOne` `AddMonoidWithOne.toOne` `SetLike.GradedMonoid.toGradedOne`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `SetLike.GradedMonoid.toGradedOne` `zero_nsmul` `LE.le.not_gt` `zero_le` `mul_apply_eq_zero` `add_comm` `add_smul` `one_smul`
`listProd_apply_eq_zero'` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`DirectSum.instMul` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DirectSum.instOne` `SetLike.gOne` `AddMonoidWithOne.toOne` `SetLike.GradedMonoid.toGradedOne`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `SetLike.GradedMonoid.toGradedOne` `LE.le.not_gt` `zero_le` `mul_apply_eq_zero`
`mul_apply_eq_zero` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DirectSum.instMul` `SetLike.gnonUnitalNonAssocSemiring` `SetLike.GradedMonoid.toGradedMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `ZeroMemClass.coe_zero` `DirectSum.coe_mul_apply` `Finset.sum_eq_zero` `lt_irrefl` `lt_of_le_of_lt` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`multisetProd_apply_eq_zero` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `Multiset.card` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Multiset.prod` `CommSemiring.toCommMonoid` `DirectSum.commSemiring` `SetLike.gcommSemiring`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `SetLike.GradedMonoid.toGradedOne` `listProd_apply_eq_zero` `Multiset.length_toList` `Multiset.coe_toList`
`multisetProd_apply_eq_zero'` 📖	mathematical	`DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `DFinsupp.instDFunLike` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoidClass.toZeroMemClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Multiset.sum` `Multiset.map`	`Multiset.prod` `CommSemiring.toCommMonoid` `DirectSum.commSemiring` `SetLike.gcommSemiring`	—	`AddSubmonoidClass.toZeroMemClass` `SetLike.GradedMonoid.toGradedMul` `SetLike.GradedMonoid.toGradedOne` `listProd_apply_eq_zero'` `Multiset.map_congr` `Multiset.coe_toList`

---

← Back to Index