Theorems · Theorem · commutative algebra

Module.Relations.Solution.ext

∀ {A : Type u} {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M}
  {inst_2 : Module A M} {x y : relations.Solution M}, x.var = y.var → x = y

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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

DFunLike.coeproof · cited by 62,936
Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
Ringstatement and proof · cited by 7,463
Finsupp.linearCombinationproof · cited by 269
Module.Relations.Gstatement and proof · cited by 103
Module.Relationsstatement and proof · cited by 97
Module.Relations.Solutionstatement and proof · cited by 70
Module.Relations.Rproof · cited by 57
Module.Relations.Solution.varstatement and proof · cited by 39
Module.Relations.relationproof · cited by 38

Cited by4

Results whose statement or proof uses this declaration.

exteriorPower.linearMap_extproof · cited by 8
Module.Relations.Solution.IsPresentationCore.isPresentationproof · cited by 5
Module.Relations.Solution.IsPresentation.postcomp_descproof · cited by 2
Module.Relations.Solution.ext_iffproof · cited by 0