Structures · Algebra
DirectSum.GSemiring
A graded version of Semiring.
- Defined in
- Mathlib.Algebra.DirectSum.Ring
- Shape
- One type argument · adds one_mul, mul_one, mul_assoc, gnpow, gnpow_zero', gnpow_succ', natCast, natCast_zero, natCast_succ
Extends2
Extended by2
Concrete types that are instances1
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- DirectSum.toSemiring
- DirectSum.GSemiring.natCast
- DirectSum.GSemiring.toGOne
- DirectSum.toSemiring_of
- DirectSum.algHom_ext'
- DirectSum.mul_eq_dfinsuppSum
- DirectSum.algebraMap_apply
- DirectSum.liftRingHom
- DirectSum.GSemiring.gnpow
- DirectSum.ringHom_ext'
- DirectSum.list_prod_ofFn_of_eq_dProd
- TensorProduct.gradedComm_algebraMap_tmul
- DirectSum.mul_eq_sum_support_ghas_mul
- DirectSum.ofList_dProd
- DirectSum.gMulLHom
- DirectSum.toAlgebra
- DirectSum.ofPow
- DirectSum.of_natCast
- DirectSum.instNatCast
- DirectSum.ofZeroRingHom
- DirectSum.GSemiring.gnpow_succ'
- DirectSum.GSemiring.toGNonUnitalNonAssocSemiring
- DirectSum.liftRingHom_apply
- DirectSum.GSemiring.natCast_zero
- DirectSum.ringHom_ext'_iff
- DirectSum.toSemiring_apply
- DirectSum.algHom_ext
- DirectSum.toSemiring.congr_simp
- DirectSum.GSemiring.toGmodule
- DirectSum.GSemiring.mul_one
- DirectSum.Gmodule.module
- DirectSum.instNatCastOfNat
- GradedMonoid.smulCommClass_right
- DirectSum.of_zero_pow
- TensorProduct.gradedComm_algebraMap
- DirectSum.semiring
- DirectSum.GSemiring.one_mul
- DirectSum.GSemiring.gnpow_zero'
- DirectSum.gMulLHom_apply_apply
- DirectSum.algebraMap_toAddMonoid_hom
- TensorProduct.gradedComm_tmul_algebraMap
- GradedMonoid.isScalarTower_right
- DirectSum.GSemiring.natCast_succ
- DirectSum.toSemiring_coe_addMonoidHom
- DirectSum.instSemiringOfNat
- TensorProduct.gradedComm_one
- DirectSum.liftRingHom_symm_apply_coe
- DirectSum.of_zero_ofNat
- DirectSum.GSemiring.mul_assoc
- DirectSum.instModuleOfNat