Ring

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

Statistics

Metric	Count
Definitions `directSumGCommRing`, `directSumGCommSemiring`, `GCommRing`, `toGCommSemiring`, `toGRing`, `GCommSemiring`, `toGCommMonoid`, `toGSemiring`, `GNonUnitalNonAssocSemiring`, `toGMul`, `GRing`, `intCast`, `toGSemiring`, `GSemiring`, `gnpow`, `natCast`, `toGMonoid`, `toGNonUnitalNonAssocSemiring`, `toGOne`, `commRing`, `commSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `semiring`, `smulWithZero`, `commRing`, `commSemiring`, `gMulHom`, `instIntCastOfNat`, `instMul`, `instNatCast`, `instNatCastOfNat`, `instNonUnitalNonAssocSemiring`, `instOne`, `liftRingHom`, `mulHom`, `nonAssocRing`, `ofZeroRingHom`, `semiring`, `toSemiring`, `directSumGNonUnitalNonAssocSemiring`, `directSumGRing`, `directSumGSemiring`	43
Theorems `mul_comm`, `mul_comm`, `add_mul`, `mul_add`, `mul_zero`, `zero_mul`, `intCast_negSucc_ofNat`, `intCast_ofNat`, `gnpow_succ'`, `gnpow_zero'`, `mul_assoc`, `mul_one`, `natCast_succ`, `natCast_zero`, `one_mul`, `gMulHom_apply_apply`, `liftRingHom_apply`, `liftRingHom_symm_apply_coe`, `list_prod_ofFn_of_eq_dProd`, `mulHom_apply`, `mulHom_of_of`, `mul_eq_dfinsuppSum`, `mul_eq_sum_support_ghas_mul`, `ofList_dProd`, `ofPow`, `of_eq_of_gradedMonoid_eq`, `of_intCast`, `of_mul_of`, `of_natCast`, `of_zero_mul`, `of_zero_ofNat`, `of_zero_one`, `of_zero_pow`, `of_zero_smul`, `one_def`, `ringHom_ext`, `ringHom_ext'`, `ringHom_ext'_iff`, `toSemiring_apply`, `toSemiring_coe_addMonoidHom`, `toSemiring_of`	41
Total	84

CommRing

Definitions

Name	Category	Theorems
`directSumGCommRing` 📖	CompOp	—

CommSemiring

Definitions

Name	Category	Theorems
`directSumGCommSemiring` 📖	CompOp	—

DirectSum

Definitions

Name	Category	Theorems
`GCommRing` 📖	CompData	—
`GCommSemiring` 📖	CompData	—
`GNonUnitalNonAssocSemiring` 📖	CompData	—
`GRing` 📖	CompData	—
`GSemiring` 📖	CompData	—
`commRing` 📖	CompOp	—
`commSemiring` 📖	CompOp	4 math math: `finsetProd_apply_eq_zero`, `multisetProd_apply_eq_zero'`, `multisetProd_apply_eq_zero`, `finsetProd_apply_eq_zero'`
`gMulHom` 📖	CompOp	1 math math: `gMulHom_apply_apply`
`instIntCastOfNat` 📖	CompOp	1 math math: `of_intCast`
`instMul` 📖	CompOp	36 math math: `mul_apply_eq_zero`, `coe_of_mul_apply_aux`, `qExpansion_of_mul`, `ExteriorAlgebra.GradedAlgebra.ι_sq_zero`, `coe_of_mul_apply_add`, `of_zero_smul`, `of_mul_of`, `coe_mul_of_apply_of_not_le`, `AddMonoidAlgebra.toDirectSum_mul`, `of_zero_mul`, `coe_mul_apply`, `toAddMonoidAlgebra_mul`, `listProd_apply_eq_zero'`, `coe_of_mul_apply_of_not_le`, `mulHom_apply`, `coe_mul_of_apply_of_mem_zero`, `coe_mul_of_apply_aux`, `decompose_symm_mul`, `coe_mul_of_apply_add`, `coe_of_mul_apply_of_le`, `coe_mul_of_apply_of_le`, `coe_of_mul_apply_of_mem_zero`, `mul_eq_sum_support_ghas_mul`, `coe_mul_of_apply`, `mul_eq_dfinsuppSum`, `TensorProduct.tmul_of_gradedMul_of_tmul`, `coe_mul_apply_eq_dfinsuppSum`, `listProd_apply_eq_zero`, `ofList_dProd`, `coe_mul_apply_eq_sum_antidiagonal`, `decompose_mul`, `list_prod_ofFn_of_eq_dProd`, `addMonoidAlgebraRingEquivDirectSum_apply`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`, `CliffordAlgebra.GradedAlgebra.ι_sq_scalar`, `coe_of_mul_apply`
`instNatCast` 📖	CompOp	3 math math: `AddMonoidAlgebra.toDirectSum_natCast`, `toAddMonoidAlgebra_natCast`, `of_natCast`
`instNatCastOfNat` 📖	CompOp	1 math math: `of_natCast`
`instNonUnitalNonAssocSemiring` 📖	CompOp	4 math math: `TensorProduct.gradedMul_def`, `ExteriorAlgebra.GradedAlgebra.ι_sq_zero`, `addMonoidAlgebraRingEquivDirectSum_apply`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`
`instOne` 📖	CompOp	14 math math: `TensorProduct.gradedComm_tmul_one`, `toAddMonoidAlgebra_one`, `one_def`, `decompose_symm_one`, `TensorProduct.algebraMap_gradedMul`, `listProd_apply_eq_zero'`, `TensorProduct.gradedMul_algebraMap`, `TensorProduct.gradedComm_one_tmul`, `listProd_apply_eq_zero`, `ofList_dProd`, `decompose_one`, `list_prod_ofFn_of_eq_dProd`, `of_zero_one`, `AddMonoidAlgebra.toDirectSum_one`
`liftRingHom` 📖	CompOp	2 math math: `liftRingHom_symm_apply_coe`, `liftRingHom_apply`
`mulHom` 📖	CompOp	2 math math: `mulHom_of_of`, `mulHom_apply`
`nonAssocRing` 📖	CompOp	—
`ofZeroRingHom` 📖	CompOp	—
`semiring` 📖	CompOp	51 math math: `TensorAlgebra.ofDirectSum_of_tprod`, `ExteriorAlgebra.GradedAlgebra.liftι_eq`, `qExpansionRingHom_apply`, `decomposeAlgEquiv_symm_apply`, `TensorAlgebra.toDirectSum_tensorPower_tprod`, `GradedTensorProduct.auxEquiv_one`, `TensorProduct.gradedComm_algebraMap_tmul`, `TensorAlgebra.toDirectSum_ofDirectSum`, `algebraMap_toAddMonoid_hom`, `AddMonoidAlgebra.decomposeAux_coe`, `ofPow`, `TensorAlgebra.equivDirectSum_apply`, `GradedTensorProduct.auxEquiv_symm_one`, `toAlgebra_apply`, `TensorProduct.gradedComm_algebraMap`, `algebraMap_apply`, `TensorProduct.algebraMap_gradedMul`, `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `TensorProduct.gradedComm_one`, `coeAlgHom_of`, `decompose_symm_algebraMap`, `TensorAlgebra.ofDirectSum_toDirectSum`, `AddMonoidAlgebra.toDirectSum_pow`, `TensorProduct.gradedMul_one`, `decompose_algebraMap`, `algHom_ext'_iff`, `toSemiring_apply`, `coeRingHom_of`, `TensorAlgebra.toDirectSum_comp_ofDirectSum`, `toSemiring_of`, `decomposeAlgEquiv_apply`, `TensorProduct.gradedComm_tmul_algebraMap`, `of_zero_pow`, `ringHom_ext'_iff`, `TensorAlgebra.equivDirectSum_symm_apply`, `TensorProduct.gradedMul_algebraMap`, `liftRingHom_symm_apply_coe`, `TensorProduct.tmul_of_gradedMul_of_tmul`, `Submodule.iSup_eq_toSubmodule_range`, `AddMonoidAlgebra.decomposeAux_single`, `toSemiring_coe_addMonoidHom`, `toAddMonoidAlgebra_pow`, `AddMonoidAlgebra.decomposeAux_eq_decompose`, `liftRingHom_apply`, `CliffordAlgebra.GradedAlgebra.lift_ι_eq`, `TensorAlgebra.toDirectSum_ι`, `TensorProduct.one_gradedMul`, `TensorAlgebra.ofDirectSum_comp_toDirectSum`, `CliffordAlgebra.GradedAlgebra.ι_sq_scalar`, `addMonoidAlgebraAlgEquivDirectSum_apply`, `qExpansion_of_pow`
`toSemiring` 📖	CompOp	5 math math: `toAlgebra_apply`, `toSemiring_apply`, `toSemiring_of`, `toSemiring_coe_addMonoidHom`, `liftRingHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gMulHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddCommMonoid` `gMulHom` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul`	—	—
`liftRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `GradedMonoid.GOne.one` `GradedMonoid.GMonoid.toGOne` `GSemiring.toGMonoid` `AddMonoidWithOne.toOne` `RingHom` `DirectSum` `semiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftRingHom` `toSemiring`	—	—
`liftRingHom_symm_apply_coe` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `GradedMonoid.GOne.one` `GradedMonoid.GMonoid.toGOne` `GSemiring.toGMonoid` `AddMonoidWithOne.toOne` `Equiv` `RingHom` `DirectSum` `semiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `liftRingHom` `AddMonoidHom.comp` `AddMonoidHomClass.toAddMonoidHom` `RingHom.instFunLike` `of`	—	—
`list_prod_ofFn_of_eq_dProd` 📖	mathematical	—	`DirectSum` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GSemiring.toGNonUnitalNonAssocSemiring` `instOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `GradedMonoid.GMonoid.toGOne` `GSemiring.toGMonoid` `DFunLike.coe` `AddMonoidHom` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `List.dProdIndex` `List.dProd`	—	`List.ofFn_eq_map` `ofList_dProd`
`mulHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddCommMonoid` `mulHom` `instMul`	—	—
`mulHom_of_of` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddCommMonoid` `mulHom` `of` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul`	—	`toAddMonoid_of`
`mul_eq_dfinsuppSum` 📖	mathematical	—	`DirectSum` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GSemiring.toGNonUnitalNonAssocSemiring` `DFinsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `of` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul`	—	`mulHom.eq_1` `toAddMonoid.eq_1` `DFinsupp.liftAddHom_apply` `DFinsupp.sumAddHom_apply` `AddMonoidHom.dfinsuppSum_apply` `GNonUnitalNonAssocSemiring.mul_zero` `GNonUnitalNonAssocSemiring.mul_add`
`mul_eq_sum_support_ghas_mul` 📖	mathematical	—	`DirectSum` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GSemiring.toGNonUnitalNonAssocSemiring` `Finset.sum` `instAddCommMonoidDirectSum` `SProd.sprod` `Finset` `Finset.instSProd` `DFinsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `of` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul` `DFinsupp` `DFinsupp.instDFunLike`	—	`mul_eq_dfinsuppSum` `Finset.sum_congr` `Finset.sum_product`
`ofList_dProd` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `List.dProdIndex` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `List.dProd` `GSemiring.toGMonoid` `instMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GSemiring.toGNonUnitalNonAssocSemiring` `instOne` `AddZero.toZero` `GradedMonoid.GMonoid.toGOne`	—	`of_mul_of`
`ofPow` 📖	mathematical	—	`DirectSum` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `AddMonoid.toNatSMul` `GradedMonoid.GMonoid.gnpow` `GSemiring.toGMonoid`	—	`of_eq_of_gradedMonoid_eq` `pow_zero` `pow_succ` `of_mul_of`
`of_eq_of_gradedMonoid_eq` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`DFinsupp.single_eq_of_sigma_eq`
`of_intCast` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DirectSum` `AddCommGroup.toAddCommMonoid` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `instIntCastOfNat` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `ring`	—	—
`of_mul_of` 📖	mathematical	—	`DirectSum` `instMul` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul`	—	`mulHom_of_of`
`of_natCast` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DirectSum` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `instNatCastOfNat` `instNatCast`	—	—
`of_zero_mul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `DirectSum` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `GradedMonoid.GradeZero.mul` `GNonUnitalNonAssocSemiring.toGMul` `AddZero.toAdd` `instMul`	—	`of_zero_smul`
`of_zero_ofNat` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DirectSum` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	`of_natCast`
`of_zero_one` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `GradedMonoid.GradeZero.one` `instOne`	—	—
`of_zero_pow` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DirectSum` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `Monoid.toNatPow` `GradedMonoid.GradeZero.monoid` `GSemiring.toGMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`pow_zero` `of_zero_one` `pow_succ` `of_zero_mul`
`of_zero_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `AddZero.toZero` `GradedMonoid.GradeZero.smul` `GNonUnitalNonAssocSemiring.toGMul` `AddZero.toAdd` `instMul`	—	`of_eq_of_gradedMonoid_eq` `GradedMonoid.mk_zero_smul` `of_mul_of`
`one_def` 📖	mathematical	—	`DirectSum` `instOne` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of` `GradedMonoid.GOne.one`	—	—
`ringHom_ext` 📖	—	`DFunLike.coe` `RingHom` `DirectSum` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `of`	—	—	`ringHom_ext'` `AddMonoidHom.ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`ringHom_ext'` 📖	—	`AddMonoidHom.comp` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `semiring` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `of`	—	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `RingHom.coe_addMonoidHom_injective` `addHom_ext'`
`ringHom_ext'_iff` 📖	mathematical	—	`AddMonoidHom.comp` `DirectSum` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `semiring` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `of`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `ringHom_ext'`
`toSemiring_apply` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `GradedMonoid.GOne.one` `GradedMonoid.GMonoid.toGOne` `GSemiring.toGMonoid` `AddMonoidWithOne.toOne` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul` `GSemiring.toGNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`RingHom` `DirectSum` `semiring` `RingHom.instFunLike` `toSemiring` `instAddCommMonoidDirectSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toAddMonoid`	—	—
`toSemiring_coe_addMonoidHom` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `GradedMonoid.GOne.one` `GradedMonoid.GMonoid.toGOne` `GSemiring.toGMonoid` `AddMonoidWithOne.toOne` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul` `GSemiring.toGNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`AddMonoidHomClass.toAddMonoidHom` `DirectSum` `RingHom` `semiring` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `toSemiring` `toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`toSemiring_of` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `GradedMonoid.GOne.one` `GradedMonoid.GMonoid.toGOne` `GSemiring.toGMonoid` `AddMonoidWithOne.toOne` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `GradedMonoid.GMul.mul` `GNonUnitalNonAssocSemiring.toGMul` `GSemiring.toGNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`RingHom` `DirectSum` `semiring` `RingHom.instFunLike` `toSemiring` `instAddCommMonoidDirectSum` `of`	—	`toAddMonoid_of`

DirectSum.GCommRing

Definitions

Name	Category	Theorems
`toGCommSemiring` 📖	CompOp	—
`toGRing` 📖	CompOp	5 math math: `qExpansionRingHom_apply`, `qExpansion_of_mul`, `ModularForm.levelOne_weight_zero_rank_one`, `mul_comm`, `qExpansion_of_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_comm` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DirectSum.GNonUnitalNonAssocSemiring.toGMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `DirectSum.GSemiring.toGNonUnitalNonAssocSemiring` `DirectSum.GRing.toGSemiring` `toGRing`	—	—

DirectSum.GCommSemiring

Definitions

Name	Category	Theorems
`toGCommMonoid` 📖	CompOp	—
`toGSemiring` 📖	CompOp	1 math math: `mul_comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_comm` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DirectSum.GNonUnitalNonAssocSemiring.toGMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `DirectSum.GSemiring.toGNonUnitalNonAssocSemiring` `toGSemiring`	—	—

DirectSum.GNonUnitalNonAssocSemiring

Definitions

Name	Category	Theorems
`toGMul` 📖	CompOp	21 math math: `DirectSum.mulHom_of_of`, `DirectSum.GSemiring.gnpow_succ'`, `DirectSum.gMulHom_apply_apply`, `DirectSum.GSemiring.mul_assoc`, `DirectSum.of_zero_smul`, `DirectSum.of_mul_of`, `mul_zero`, `DirectSum.of_zero_mul`, `DirectSum.GCommRing.mul_comm`, `add_mul`, `DirectSum.GAlgebra.map_mul`, `DirectSum.GSemiring.one_mul`, `DirectSum.GCommSemiring.mul_comm`, `DirectSum.GAlgebra.smul_def`, `DirectSum.mul_eq_sum_support_ghas_mul`, `DirectSum.mul_eq_dfinsuppSum`, `DirectSum.GAlgebra.commutes`, `zero_mul`, `mul_add`, `DirectSum.GSemiring.mul_one`, `DirectSum.gMulLHom_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mul` 📖	mathematical	—	`GradedMonoid.GMul.mul` `toGMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`mul_add` 📖	mathematical	—	`GradedMonoid.GMul.mul` `toGMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`mul_zero` 📖	mathematical	—	`GradedMonoid.GMul.mul` `toGMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`zero_mul` 📖	mathematical	—	`GradedMonoid.GMul.mul` `toGMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—

DirectSum.GRing

Definitions

Name	Category	Theorems
`intCast` 📖	CompOp	2 math math: `intCast_ofNat`, `intCast_negSucc_ofNat`
`toGSemiring` 📖	CompOp	13 math math: `qExpansionRingHom_apply`, `TensorProduct.gradedMul_def`, `qExpansion_of_mul`, `ModularForm.levelOne_weight_zero_rank_one`, `TensorProduct.algebraMap_gradedMul`, `intCast_ofNat`, `DirectSum.GCommRing.mul_comm`, `TensorProduct.gradedMul_one`, `TensorProduct.gradedMul_algebraMap`, `TensorProduct.tmul_of_gradedMul_of_tmul`, `TensorProduct.one_gradedMul`, `intCast_negSucc_ofNat`, `qExpansion_of_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intCast_negSucc_ofNat` 📖	mathematical	—	`intCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DirectSum.GSemiring.natCast` `AddCommGroup.toAddCommMonoid` `toGSemiring`	—	—
`intCast_ofNat` 📖	mathematical	—	`intCast` `DirectSum.GSemiring.natCast` `AddCommGroup.toAddCommMonoid` `toGSemiring`	—	—

DirectSum.GSemiring

Definitions

Name	Category	Theorems
`gnpow` 📖	CompOp	2 math math: `gnpow_succ'`, `gnpow_zero'`
`natCast` 📖	CompOp	4 math math: `DirectSum.GRing.intCast_ofNat`, `natCast_zero`, `natCast_succ`, `DirectSum.GRing.intCast_negSucc_ofNat`
`toGMonoid` 📖	CompOp	11 math math: `DirectSum.ofPow`, `TensorProduct.algebraMap_gradedMul`, `GradedMonoid.smulCommClass_right`, `DirectSum.of_zero_pow`, `TensorProduct.gradedMul_algebraMap`, `DirectSum.liftRingHom_symm_apply_coe`, `DirectSum.ofList_dProd`, `GradedMonoid.isScalarTower_right`, `DirectSum.GAlgebra.map_one`, `DirectSum.list_prod_ofFn_of_eq_dProd`, `DirectSum.liftRingHom_apply`
`toGNonUnitalNonAssocSemiring` 📖	CompOp	18 math math: `gnpow_succ'`, `TensorProduct.gradedMul_def`, `mul_assoc`, `qExpansion_of_mul`, `ModularForm.levelOne_weight_zero_rank_one`, `DirectSum.GCommRing.mul_comm`, `DirectSum.GAlgebra.map_mul`, `one_mul`, `DirectSum.GCommSemiring.mul_comm`, `DirectSum.GAlgebra.smul_def`, `DirectSum.mul_eq_sum_support_ghas_mul`, `DirectSum.mul_eq_dfinsuppSum`, `TensorProduct.tmul_of_gradedMul_of_tmul`, `DirectSum.ofList_dProd`, `DirectSum.GAlgebra.commutes`, `DirectSum.list_prod_ofFn_of_eq_dProd`, `mul_one`, `DirectSum.gMulLHom_apply_apply`
`toGOne` 📖	CompOp	4 math math: `gnpow_zero'`, `one_mul`, `natCast_succ`, `mul_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gnpow_succ'` 📖	mathematical	—	`AddMonoid.toNatSMul` `gnpow` `GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DirectSum.GNonUnitalNonAssocSemiring.toGMul` `toGNonUnitalNonAssocSemiring`	—	—
`gnpow_zero'` 📖	mathematical	—	`AddMonoid.toNatSMul` `gnpow` `GradedMonoid` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toGOne`	—	—
`mul_assoc` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DirectSum.GNonUnitalNonAssocSemiring.toGMul` `toGNonUnitalNonAssocSemiring`	—	—
`mul_one` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DirectSum.GNonUnitalNonAssocSemiring.toGMul` `toGNonUnitalNonAssocSemiring` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toGOne`	—	—
`natCast_succ` 📖	mathematical	—	`natCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `GradedMonoid.GOne.one` `toGOne`	—	—
`natCast_zero` 📖	mathematical	—	`natCast` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`one_mul` 📖	mathematical	—	`GradedMonoid` `GradedMonoid.GMul.toMul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DirectSum.GNonUnitalNonAssocSemiring.toGMul` `toGNonUnitalNonAssocSemiring` `GradedMonoid.GOne.toOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toGOne`	—	—

DirectSum.GradeZero

Definitions

Name	Category	Theorems
`commRing` 📖	CompOp	—
`commSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalNonAssocSemiring` 📖	CompOp	1 math math: `ModularForm.levelOne_weight_zero_rank_one`
`semiring` 📖	CompOp	—
`smulWithZero` 📖	CompOp	—

NonUnitalNonAssocSemiring

Definitions

Name	Category	Theorems
`directSumGNonUnitalNonAssocSemiring` 📖	CompOp	4 math math: `AddMonoidAlgebra.toDirectSum_mul`, `DirectSum.toAddMonoidAlgebra_mul`, `addMonoidAlgebraRingEquivDirectSum_apply`, `addMonoidAlgebraRingEquivDirectSum_symm_apply`

Ring

Definitions

Name	Category	Theorems
`directSumGRing` 📖	CompOp	2 math math: `AddMonoidAlgebra.toDirectSum_intCast`, `DirectSum.toAddMonoidAlgebra_intCast`

Semiring

Definitions

Name	Category	Theorems
`directSumGSemiring` 📖	CompOp	7 math math: `Algebra.directSumGAlgebra_toFun_apply`, `AddMonoidAlgebra.toDirectSum_natCast`, `addMonoidAlgebraAlgEquivDirectSum_symm_apply`, `DirectSum.toAddMonoidAlgebra_natCast`, `AddMonoidAlgebra.toDirectSum_pow`, `DirectSum.toAddMonoidAlgebra_pow`, `addMonoidAlgebraAlgEquivDirectSum_apply`

---

← Back to Index