Structures · Algebra
DirectSum.GAlgebra
A graded version of Algebra. An instance of DirectSum.GAlgebra R A endows (⨁ i, A i)
with an R-algebra structure.
- Defined in
- Mathlib.Algebra.DirectSum.Algebra
- Shape
- 2 explicit arguments · adds toFun, map_one, map_mul, commutes, smul_def
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- DirectSum.GAlgebra.toFun
- TensorProduct.gradedMul
- TensorProduct.tmul_of_gradedMul_of_tmul
- DirectSum.algHom_ext'
- DirectSum.algebraMap_apply
- TensorProduct.gradedMul_def
- TensorProduct.gradedMul_algebraMap
- TensorProduct.gradedComm_algebraMap_tmul
- TensorProduct.algebraMap_gradedMul
- DirectSum.gMulLHom
- DirectSum.toAlgebra
- DirectSum.GAlgebra.smul_def
- DirectSum.algHom_ext
- GradedMonoid.smulCommClass_right
- TensorProduct.gradedComm_algebraMap
- TensorProduct.one_gradedMul
- DirectSum.GAlgebra.map_one
- DirectSum.gMulLHom_apply_apply
- DirectSum.algebraMap_toAddMonoid_hom
- TensorProduct.gradedComm_tmul_algebraMap
- TensorProduct.gradedComm_gradedMul
- DirectSum.GAlgebra.commutes
- GradedMonoid.isScalarTower_right
- TensorProduct.gradedMul_assoc
- DirectSum.GAlgebra.map_mul
- TensorProduct.gradedMul_one
- DirectSum.algHom_ext'_iff
- DirectSum.instAlgebra
- DirectSum.toAlgebra_apply
Ancestors0
No ancestors.