DirectSum

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

Statistics

Metric	Count
Definitions directSum, finsupp, isRepresentationCore, directSum, directSumEquiv, directSum	6
Theorems directSum_G, directSum_R, directSum_relation, directSum_var, finsupp_G, finsupp_R, finsupp_relation, finsupp_var, directSum, directSumEquiv_apply_var, directSumEquiv_symm_apply_var, directSum_var, directSum_G, directSum_R, directSum_relation	15
Total	21

Module.Presentation

Definitions

Name	Category	Theorems
directSum 📖	CompOp	4 math math: directSum_var, directSum_relation, directSum_G, directSum_R
finsupp 📖	CompOp	4 math math: finsupp_R, finsupp_G, finsupp_var, finsupp_relation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum_G 📖	mathematical	—	Module.Relations.G toRelations DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule Ring.toSemiring directSum	—	—
directSum_R 📖	mathematical	—	Module.Relations.R toRelations DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule Ring.toSemiring directSum	—	—
directSum_relation 📖	mathematical	—	Module.Relations.relation toRelations DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule Ring.toSemiring directSum Finsupp.embDomain Module.Relations.G Module.Relations.R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Function.Embedding.sigmaMk	—	—
directSum_var 📖	mathematical	—	Module.Relations.Solution.var toRelations DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule Ring.toSemiring directSum toSolution Module.Relations.G DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoidDirectSum LinearMap.instFunLike DirectSum.lof	—	—
finsupp_G 📖	mathematical	—	Module.Relations.G toRelations Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid finsupp	—	—
finsupp_R 📖	mathematical	—	Module.Relations.R toRelations Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid finsupp	—	—
finsupp_relation 📖	mathematical	—	Module.Relations.relation toRelations Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid finsupp Finsupp.embDomain Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Function.Embedding.sigmaMk Module.Relations.R	—	—
finsupp_var 📖	mathematical	—	Module.Relations.Solution.var toRelations Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAddCommGroup Finsupp.module Ring.toSemiring AddCommGroup.toAddCommMonoid finsupp toSolution Module.Relations.G Finsupp.single	—	LinearEquiv.injective RingHomInvPair.ids LinearEquiv.apply_symm_apply directSum_var finsuppLequivDFinsupp_apply_apply Finsupp.toDFinsupp_single

Module.Relations

Definitions

Name	Category	Theorems
directSum 📖	CompOp	7 math math: directSum_G, Solution.directSumEquiv_apply_var, Solution.directSum_var, Solution.directSumEquiv_symm_apply_var, directSum_R, Solution.IsPresentation.directSum, directSum_relation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum_G 📖	mathematical	—	G directSum	—	—
directSum_R 📖	mathematical	—	R directSum	—	—
directSum_relation 📖	mathematical	—	relation directSum Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.embDomain Function.Embedding.sigmaMk	—	—

Module.Relations.Solution

Definitions

Name	Category	Theorems
directSum 📖	CompOp	2 math math: directSum_var, IsPresentation.directSum
directSumEquiv 📖	CompOp	2 math math: directSumEquiv_apply_var, directSumEquiv_symm_apply_var

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSumEquiv_apply_var 📖	mathematical	—	var DFunLike.coe Equiv Module.Relations.Solution Module.Relations.directSum EquivLike.toFunLike Equiv.instEquivLike directSumEquiv Module.Relations.G	—	—
directSumEquiv_symm_apply_var 📖	mathematical	—	var Module.Relations.directSum DFunLike.coe Equiv Module.Relations.Solution EquivLike.toFunLike Equiv.instEquivLike Equiv.symm directSumEquiv	—	—
directSum_var 📖	mathematical	—	var Module.Relations.directSum DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule Ring.toSemiring directSum Module.Relations.G DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoidDirectSum LinearMap.instFunLike DirectSum.lof	—	—

Module.Relations.Solution.IsPresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum 📖	mathematical	Module.Relations.Solution.IsPresentation	Module.Relations.directSum DirectSum AddCommGroup.toAddCommMonoid DirectSum.instAddCommGroup DirectSum.instModule Ring.toSemiring Module.Relations.Solution.directSum	—	Module.Relations.Solution.IsPresentationCore.isPresentation

Module.Relations.Solution.IsPresentation.directSum

Definitions

Name	Category	Theorems
isRepresentationCore 📖	CompOp	—

---

← Back to Index