Mathlib Map

Theorems · Definition · commutative algebra

Module.Relations.G

{A : Type u} → [inst : Ring A] → Module.Relations A → Type w₀

the index type for generators

Defined in
Mathlib.Algebra.Module.Presentation.Basic
Cited by
103 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Assumes
Ring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Module.Relations.Solution.var · cited by 39Solution.varModule.Relations.relation · cited by 38Relations.relationModule.Relations.Solution.π · cited by 30Solution.πModule.Relations.Quotient · cited by 22Relations.QuotientModule.Relations.Solution.postcomp · cited by 17Solution.postcompModule.Relations.toQuotient · cited by 15Relations.toQuotientModule.Relations.map · cited by 12Relations.mapexteriorPower.linearMap_ext · cited by 8exteriorPower.linearMap_e…Module.Relations.Solution.π_single · cited by 7Solution.π_singleModule.Relations.directSum · cited by 7Relations.directSumModule.Presentation.cokernelRelations · cited by 6Presentation.cokernelRela…Module.Relations.tensor · cited by 6Relations.tensorModule.Relations.Solution.IsPresentationCore.isPresentation · cited by 5IsPresentationCore.isPres…Module.Presentation.CokernelData.lift · cited by 5CokernelData.liftModule.Relations.Quotient.linearMap_ext · cited by 5Quotient.linearMap_extRing · cited by 7463RingModule.Relations · cited by 97Module.RelationsRelations.GCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by138

Results whose statement or proof uses this declaration.