Algebra

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

Statistics

Metric	Count
Definitions directSumGAlgebra, GAlgebra, toFun, gMulLHom, instAlgebra, toAlgebra	6
Theorems directSumGAlgebra_toFun_apply, commutes, map_mul, map_one, smul_def, algHom_ext, algHom_ext', algHom_ext'_iff, algebraMap_apply, algebraMap_toAddMonoid_hom, gMulLHom_apply_apply, toAlgebra_apply, isScalarTower_right, smulCommClass_right	14
Total	20

Algebra

Definitions

Name	Category	Theorems
directSumGAlgebra 📖	CompOp	3 math math: directSumGAlgebra_toFun_apply, addMonoidAlgebraAlgEquivDirectSum_symm_apply, addMonoidAlgebraAlgEquivDirectSum_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSumGAlgebra_toFun_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidHom.instFunLike DirectSum.GAlgebra.toFun NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Semiring.directSumGSemiring directSumGAlgebra OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.toOneHom RingHom.toMonoidHom algebraMap	—	—

DirectSum

Definitions

Name	Category	Theorems
GAlgebra 📖	CompData	—
gMulLHom 📖	CompOp	1 math math: gMulLHom_apply_apply
instAlgebra 📖	CompOp	33 math math: TensorAlgebra.ofDirectSum_of_tprod, ExteriorAlgebra.GradedAlgebra.liftι_eq, decomposeAlgEquiv_symm_apply, TensorAlgebra.toDirectSum_tensorPower_tprod, TensorProduct.gradedComm_algebraMap_tmul, TensorAlgebra.toDirectSum_ofDirectSum, algebraMap_toAddMonoid_hom, AddMonoidAlgebra.decomposeAux_coe, TensorAlgebra.equivDirectSum_apply, toAlgebra_apply, TensorProduct.gradedComm_algebraMap, algebraMap_apply, TensorProduct.algebraMap_gradedMul, addMonoidAlgebraAlgEquivDirectSum_symm_apply, coeAlgHom_of, decompose_symm_algebraMap, TensorAlgebra.ofDirectSum_toDirectSum, decompose_algebraMap, algHom_ext'_iff, TensorAlgebra.toDirectSum_comp_ofDirectSum, decomposeAlgEquiv_apply, TensorProduct.gradedComm_tmul_algebraMap, TensorAlgebra.equivDirectSum_symm_apply, TensorProduct.gradedMul_algebraMap, TensorProduct.tmul_of_gradedMul_of_tmul, Submodule.iSup_eq_toSubmodule_range, AddMonoidAlgebra.decomposeAux_single, AddMonoidAlgebra.decomposeAux_eq_decompose, CliffordAlgebra.GradedAlgebra.lift_ι_eq, TensorAlgebra.toDirectSum_ι, TensorAlgebra.ofDirectSum_comp_toDirectSum, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, addMonoidAlgebraAlgEquivDirectSum_apply
toAlgebra 📖	CompOp	1 math math: toAlgebra_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	DFunLike.coe AlgHom DirectSum semiring instAlgebra AlgHom.funLike AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike of	—	—	algHom_ext' LinearMap.ext RingHomCompTriple.ids
algHom_ext' 📖	—	LinearMap.comp DirectSum CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Algebra.toModule instAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap lof	—	—	RingHomCompTriple.ids AlgHom.toLinearMap_injective linearMap_ext
algHom_ext'_iff 📖	mathematical	—	LinearMap.comp DirectSum CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Algebra.toModule instAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap lof	—	RingHomCompTriple.ids algHom_ext'
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom DirectSum Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap instAlgebra AddMonoidHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike of AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne GAlgebra.toFun	—	—
algebraMap_toAddMonoid_hom 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom DirectSum RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum RingHom.instFunLike RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass algebraMap instAlgebra AddMonoidHom.comp AddZero.toZero of GAlgebra.toFun	—	RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
gMulLHom_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddSemigroup.toAdd AddMonoid.toAddSemigroup LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction gMulLHom GradedMonoid.GMul.mul GNonUnitalNonAssocSemiring.toGMul GSemiring.toGNonUnitalNonAssocSemiring	—	smulCommClass_self
toAlgebra_apply 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike GradedMonoid.GOne.one GradedMonoid.GMonoid.toGOne GSemiring.toGMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSemigroup.toAdd AddMonoid.toAddSemigroup GradedMonoid.GMul.mul GNonUnitalNonAssocSemiring.toGMul GSemiring.toGNonUnitalNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	AlgHom DirectSum semiring instAlgebra AlgHom.funLike toAlgebra RingHom RingHom.instFunLike toSemiring LinearMap.toAddMonoidHom	—	—

DirectSum.GAlgebra

Definitions

Name	Category	Theorems
toFun 📖	CompOp	10 math math: DirectSum.algebraMap_toAddMonoid_hom, Algebra.directSumGAlgebra_toFun_apply, DirectSum.algebraMap_apply, TensorPower.galgebra_toFun_def, Submodule.setLike.coe_galgebra_toFun, map_mul, smul_def, commutes, map_one, TensorPower.toTensorAlgebra_galgebra_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutes 📖	mathematical	—	GradedMonoid GradedMonoid.GMul.toMul AddSemigroup.toAdd AddMonoid.toAddSemigroup DirectSum.GNonUnitalNonAssocSemiring.toGMul DirectSum.GSemiring.toGNonUnitalNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DFunLike.coe AddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike toFun	—	—
map_mul 📖	mathematical	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DFunLike.coe AddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike toFun Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddSemigroup.toAdd AddMonoid.toAddSemigroup GradedMonoid.GMul.mul DirectSum.GNonUnitalNonAssocSemiring.toGMul DirectSum.GSemiring.toGNonUnitalNonAssocSemiring	—	—
map_one 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike toFun AddMonoidWithOne.toOne GradedMonoid.GOne.one GradedMonoid.GMonoid.toGOne DirectSum.GSemiring.toGMonoid	—	—
smul_def 📖	mathematical	—	GradedMonoid GradedMonoid.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction GradedMonoid.GMul.toMul AddSemigroup.toAdd AddMonoid.toAddSemigroup DirectSum.GNonUnitalNonAssocSemiring.toGMul DirectSum.GSemiring.toGNonUnitalNonAssocSemiring DFunLike.coe AddMonoidHom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoidHom.instFunLike toFun	—	—

GradedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isScalarTower_right 📖	mathematical	—	IsScalarTower GradedMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction SemigroupAction.toSMul Monoid.toSemigroup GMonoid.toMonoid DirectSum.GSemiring.toGMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	DirectSum.GAlgebra.smul_def mul_assoc
smulCommClass_right 📖	mathematical	—	SMulCommClass GradedMonoid instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction SemigroupAction.toSMul Monoid.toSemigroup GMonoid.toMonoid DirectSum.GSemiring.toGMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	DirectSum.GAlgebra.smul_def mul_assoc DirectSum.GAlgebra.commutes

---

← Back to Index