Theorems · Definition · commutative algebra
Module.presentationFinsupp
(A : Type u) → [inst : Ring A] → (G : Type w₀) → Module.Presentation A (G →₀ A)
The presentation of the A-module G →₀ A with generators indexed by G,
and no relation. (Note that there is an auxiliary universe parameter w₁ for the
empty type R.)
- Defined in
- Mathlib.Algebra.Module.Presentation.Free
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Finsuppstatement and proof · cited by 5,255
- Module.Relations.Solutionproof · cited by 70
- Module.Presentationstatement · cited by 40
- Module.Relations.Solution.IsPresentationproof · cited by 39
- Module.Relations.solutionFinsuppproof · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- Module.free_iff_exists_presentationproof · cited by 0
- Module.presentationFinsupp_Gstatement and proof · cited by 0
- Module.presentationFinsupp_Rstatement and proof · cited by 0
- Module.presentationFinsupp_varstatement and proof · cited by 0