Theorems · Definition · commutative algebra

Module.Relations.map

{A : Type u} → [inst : Ring A] → (relations : Module.Relations A) → (relations.R →₀ A) →ₗ[A] relations.G →₀ A

The linear map (relations.R →₀ A) →ₗ[A] (relations.G →₀ A) corresponding to the relations given by relations : Relations A.

Defined in: Mathlib.Algebra.Module.Presentation.Basic
Cited by: 12 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

RingHom.idstatement · cited by 18,349
LinearMapstatement · cited by 10,215
Ringstatement and proof · cited by 7,463
Finsuppstatement · cited by 5,255
Finsupp.linearCombinationproof · cited by 269
Module.Relations.Gstatement · cited by 103
Module.Relationsstatement and proof · cited by 97
Module.Relations.Rstatement · cited by 57
Module.Relations.relationproof · cited by 38

Cited by14

Results whose statement or proof uses this declaration.

Module.Relations.map_singlestatement · cited by 3
Module.Relations.range_mapstatement · cited by 3
Module.Relations.Solution.ofπ'statement and proof · cited by 2
Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_spanproof · cited by 2
Module.Relations.toQuotient_map_applystatement · cited by 1
Algebra.Presentation.differentials.comm₁₂statement and proof · cited by 1
Module.Relations.Solution.π_comp_mapstatement · cited by 1
Module.Relations.toQuotient_mapstatement · cited by 1
Module.Relations.Solution.π_comp_map_applystatement · cited by 0
Algebra.Presentation.differentialsSolution_isPresentationproof · cited by 0
Module.Relations.Solution.ofπ'_varstatement and proof · cited by 0
Module.Relations.Solution.ofπ'_πstatement and proof · cited by 0