Loogle!

Result

Found 89 declarations mentioning Module.Relations.Solution.

• Module.Relations.Solution 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] (relations : Module.Relations A) (M : Type v) [AddCommGroup M] [Module A M] : Type (max v w₀)
• Module.Relations.Solution.ofQuotient 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] (relations : Module.Relations A) : relations.Solution relations.Quotient
• Module.Relations.Solution.IsPresentation 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Prop
• Module.Relations.Solution.IsPresentationCore 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Type (max (max (max u v) (w' + 1)) w₀)
• Module.Relations.Solution.var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (self : relations.Solution M) (g : relations.G) : M
• Module.Presentation.toSolution 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (self : Module.Presentation A M) : self.Solution M
• Module.Presentation.mk 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (toRelations : Module.Relations A) (toSolution : toRelations.Solution M) (toIsPresentation : toSolution.IsPresentation) : Module.Presentation A M
• Module.Presentation.ofIsPresentation 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) : Module.Presentation A M
• Module.Relations.Solution.IsPresentationCore.down 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) : solution.IsPresentationCore
• Module.Relations.Solution.IsPresentationCore.isPresentation 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) : solution.IsPresentation
• Module.Presentation.ofIsPresentation_toRelations 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) : (Module.Presentation.ofIsPresentation h).toRelations = relations
• Module.Relations.Solution.postcomp_id 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.postcomp LinearMap.id = solution
• Module.Presentation.ofIsPresentation_toSolution 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) : (Module.Presentation.ofIsPresentation h).toSolution = solution
• Module.Relations.Solution.fromQuotient 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : relations.Quotient →ₗ[A] M
• Module.Relations.Solution.ext 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} {inst✝ : Ring A} {relations : Module.Relations A} {M : Type v} {inst✝¹ : AddCommGroup M} {inst✝² : Module A M} {x y : relations.Solution M} (var : x.var = y.var) : x = y
• Module.Relations.Solution.ext_iff 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} {inst✝ : Ring A} {relations : Module.Relations A} {M : Type v} {inst✝¹ : AddCommGroup M} {inst✝² : Module A M} {x y : relations.Solution M} : x = y ↔ x.var = y.var
• Module.Relations.Solution.congr_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution solution' : relations.Solution M} (h : solution = solution') (g : relations.G) : solution.var g = solution'.var g
• Module.Relations.Solution.postcomp 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : relations.Solution N
• Module.Relations.Solution.IsPresentation.desc 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : M →ₗ[A] N
• Module.Relations.Solution.IsPresentationCore.desc 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : M →ₗ[A] N
• Module.Relations.Solution.IsPresentation.linearMapEquiv 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] : (M →ₗ[A] N) ≃ relations.Solution N
• Module.Relations.Solution.IsPresentation.postcomp_desc 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : solution.postcomp (h.desc s) = s
• Module.Relations.Solution.IsPresentationCore.postcomp_desc 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : solution.postcomp (self.desc s) = s
• Module.Relations.Solution.IsPresentation.linearEquiv 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) : relations.Quotient ≃ₗ[A] M
• Module.Relations.Solution.π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : (relations.G →₀ A) →ₗ[A] M
• Module.Relations.Solution.IsPresentation.uniq 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) : M ≃ₗ[A] N
• Module.Relations.Solution.congr_postcomp 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution M} (h : solution = solution') (f : M →ₗ[A] N) : solution.postcomp f = solution'.postcomp f
• Module.Relations.Solution.IsPresentation.bijective 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentation) : Function.Bijective ⇑solution.fromQuotient
• Module.Relations.Solution.IsPresentation.mk 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (bijective : Function.Bijective ⇑solution.fromQuotient) : solution.IsPresentation
• Module.Relations.Solution.IsPresentation.postcomp_uniq 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) : solution.postcomp ↑(h.uniq h') = solution'
• Module.Relations.Solution.range_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.π.range = Submodule.span A (Set.range solution.var)
• Module.Relations.Solution.IsPresentation.desc_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) (g : relations.G) : (h.desc s) (solution.var g) = s.var g
• Module.Relations.Solution.IsPresentationCore.desc_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] (s : relations.Solution N) (g : relations.G) : (h.desc s) (solution.var g) = s.var g
• Module.Relations.Solution.IsPresentation.of_linearEquiv 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) : (solution.postcomp ↑e).IsPresentation
• Module.Relations.Solution.postcomp_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (g : relations.G) : (solution.postcomp f).var g = f (solution.var g)
• Module.Relations.Solution.IsPresentation.postcomp_injective 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {f f' : M →ₗ[A] N} (h' : solution.postcomp f = solution.postcomp f') : f = f'
• Module.Relations.Solution.IsPresentationCore.postcomp_injective 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] {f f' : M →ₗ[A] N} (h : solution.postcomp f = solution.postcomp f') : f = f'
• Module.Presentation.ofLinearEquiv_toSolution 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Module.Presentation A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) : (pres.ofLinearEquiv e).toSolution = pres.postcomp ↑e
• Module.Relations.Solution.IsPresentation.postcomp_uniq_symm 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) : solution'.postcomp ↑(h.uniq h').symm = solution
• Module.Relations.Solution.postcomp_comp 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) {N' : Type v''} [AddCommGroup N'] [Module A N'] (g : N →ₗ[A] N') : solution.postcomp (g ∘ₗ f) = (solution.postcomp f).postcomp g
• Module.Relations.Solution.IsPresentation.surjective_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) : Function.Surjective ⇑solution.π
• Module.Relations.Solution.π_relation 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (r : relations.R) : solution.π (relations.relation r) = 0
• Module.Relations.Solution.fromQuotient_comp_toQuotient 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.fromQuotient ∘ₗ relations.toQuotient = solution.π
• Module.Relations.Solution.IsPresentation.ker_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) : solution.π.ker = Submodule.span A (Set.range relations.relation)
• Module.Relations.Solution.mk 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (var : relations.G → M) (linearCombination_var_relation : ∀ (r : relations.R), (Finsupp.linearCombination A var) (relations.relation r) = 0) : relations.Solution M
• Module.Relations.Solution.linearCombination_var_relation 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (self : relations.Solution M) (r : relations.R) : (Finsupp.linearCombination A self.var) (relations.relation r) = 0
• Module.Relations.Solution.π_single 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (g : relations.G) : (solution.π fun₀ | g => 1) = solution.var g
• Module.Relations.Solution.IsPresentation.uniq_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) (g : relations.G) : (h.uniq h') (solution.var g) = solution'.var g
• Module.Relations.Solution.IsPresentationCore.mk 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (desc : {N : Type w'} → [inst : AddCommGroup N] → [inst_1 : Module A N] → relations.Solution N → M →ₗ[A] N) (postcomp_desc : ∀ {N : Type w'} [inst : AddCommGroup N] [inst_1 : Module A N] (s : relations.Solution N), solution.postcomp (desc s) = s) (postcomp_injective : ∀ {N : Type w'} [inst : AddCommGroup N] [inst_1 : Module A N] {f f' : M →ₗ[A] N}, solution.postcomp f = solution.postcomp f' → f = f') : solution.IsPresentationCore
• Module.Relations.Solution.IsPresentation.desc_comp_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : h.desc s ∘ₗ solution.π = s.π
• Module.Relations.Solution.surjective_π_iff_span_eq_top 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Function.Surjective ⇑solution.π ↔ Submodule.span A (Set.range solution.var) = ⊤
• Module.Relations.Solution.ofπ 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (r : relations.R), π (relations.relation r) = 0) : relations.Solution M
• Module.Relations.Solution.IsPresentation.uniq_symm_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) (g : relations.G) : (h.uniq h').symm (solution'.var g) = solution.var g
• Module.Relations.Solution.isPresentation_mk 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (h₁ : Submodule.span A (Set.range solution.var) = ⊤) (h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)) : solution.IsPresentation
• Module.Relations.Solution.isPresentation_iff 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.IsPresentation ↔ Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)
• Module.Relations.Solution.IsPresentation.linearMapEquiv_apply 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) : h.linearMapEquiv f = solution.postcomp f
• Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Function.Surjective ⇑solution.fromQuotient ↔ Function.Surjective ⇑solution.π
• Module.Relations.Solution.IsPresentation.linearMapEquiv_symm_apply 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : h.linearMapEquiv.symm s = h.desc s
• Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Function.Injective ⇑solution.fromQuotient ↔ solution.π.ker = Submodule.span A (Set.range relations.relation)
• Module.Relations.Solution.IsPresentation.linearEquiv_apply 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) (x : relations.Quotient) : h.linearEquiv x = solution.fromQuotient x
• Module.Relations.Solution.span_relation_le_ker_π 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Submodule.span A (Set.range relations.relation) ≤ solution.π.ker
• Module.Relations.Solution.π_comp_map 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.π ∘ₗ relations.map = 0
• Module.Relations.Solution.IsPresentation.π_desc_apply 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) (x : relations.G →₀ A) : (h.desc s) (solution.π x) = s.π x
• Module.Relations.Solution.π_comp_map_apply 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (x : relations.R →₀ A) : solution.π (relations.map x) = 0
• Module.Relations.Solution.IsPresentation.exact 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) : Function.Exact ⇑relations.map ⇑solution.π
• Module.Relations.Solution.fromQuotient_toQuotient 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (x : relations.G →₀ A) : solution.fromQuotient (relations.toQuotient x) = solution.π x
• Module.Relations.Solution.ofπ' 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0) : relations.Solution M
• Module.Relations.Solution.IsPresentation.linearEquiv_symm_var 📋 Mathlib.Algebra.Module.Presentation.Basic
  {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) (g : relations.G) : h.linearEquiv.symm (solution.var g) = relations.toQuotient fun₀ | g => 1
• exteriorPower.presentation.relationsSolutionEquiv 📋 Mathlib.LinearAlgebra.ExteriorPower.Basic
  {R : Type u} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {ι : Type u_4} [DecidableEq ι] {M : Type u_5} [AddCommGroup M] [Module R M] : (exteriorPower.presentation.relations R ι M).Solution N ≃ M [⋀^ι]→ₗ[R] N
• exteriorPower.presentation.relationsSolutionEquiv_apply_apply 📋 Mathlib.LinearAlgebra.ExteriorPower.Basic
  {R : Type u} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {ι : Type u_4} [DecidableEq ι] {M : Type u_5} [AddCommGroup M] [Module R M] (s : (exteriorPower.presentation.relations R ι M).Solution N) (m : ι → M) : (exteriorPower.presentation.relationsSolutionEquiv s) m = s.var m
• exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var 📋 Mathlib.LinearAlgebra.ExteriorPower.Basic
  {R : Type u} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {ι : Type u_4} [DecidableEq ι] {M : Type u_5} [AddCommGroup M] [Module R M] (f : M [⋀^ι]→ₗ[R] N) (m : (exteriorPower.presentation.relations R ι M).G) : (exteriorPower.presentation.relationsSolutionEquiv.symm f).var m = f m
• exteriorPower.presentation.isPresentationCore 📋 Mathlib.LinearAlgebra.ExteriorPower.Basic
  (R : Type u) [CommRing R] (n : ℕ) (M : Type u_1) [AddCommGroup M] [Module R M] : (exteriorPower.presentation.relationsSolutionEquiv.symm (exteriorPower.ιMulti R n)).IsPresentationCore
• Module.Presentation.cokernelSolution 📋 Mathlib.Algebra.Module.Presentation.Cokernel
  {A : Type u} [Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁} {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) : (pres₂.cokernelRelations data).Solution (M₂ ⧸ f.range)
• Algebra.Presentation.differentialsSolution 📋 Mathlib.Algebra.Module.Presentation.Differentials
  {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Algebra.Presentation R S ι σ) : pres.differentialsRelations.Solution Ω[S⁄R]
• Module.Relations.Solution.directSumEquiv 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} {relations : ι → Module.Relations A} {N : Type v} [AddCommGroup N] [Module A N] : (Module.Relations.directSum relations).Solution N ≃ ((i : ι) → (relations i).Solution N)
• Module.Relations.Solution.directSum 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (solution : (i : ι) → (relations i).Solution (M i)) : (Module.Relations.directSum relations).Solution (DirectSum ι fun i => M i)
• Module.Relations.Solution.IsPresentation.directSum 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] {solution : (i : ι) → (relations i).Solution (M i)} (h : ∀ (i : ι), (solution i).IsPresentation) : (Module.Relations.Solution.directSum solution).IsPresentation
• Module.Relations.Solution.IsPresentation.directSum.isRepresentationCore 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] {solution : (i : ι) → (relations i).Solution (M i)} (h : ∀ (i : ι), (solution i).IsPresentation) : (Module.Relations.Solution.directSum solution).IsPresentationCore
• Module.Relations.Solution.directSumEquiv_apply_var 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} {relations : ι → Module.Relations A} {N : Type v} [AddCommGroup N] [Module A N] (s : (Module.Relations.directSum relations).Solution N) (i : ι) (g : (relations i).G) : (Module.Relations.Solution.directSumEquiv s i).var g = s.var ⟨i, g⟩
• Module.Relations.Solution.directSumEquiv_symm_apply_var 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} {relations : ι → Module.Relations A} {N : Type v} [AddCommGroup N] [Module A N] (t : (i : ι) → (relations i).Solution N) (x✝ : (Module.Relations.directSum relations).G) : (Module.Relations.Solution.directSumEquiv.symm t).var x✝ = match x✝ with | ⟨i, g⟩ => (t i).var g
• Module.Relations.Solution.directSum_var 📋 Mathlib.Algebra.Module.Presentation.DirectSum
  {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (solution : (i : ι) → (relations i).Solution (M i)) (i : ι) (g : (relations i).G) : (Module.Relations.Solution.directSum solution).var ⟨i, g⟩ = (DirectSum.lof A ι M i) ((solution i).var g)
• Module.Relations.Solution.IsPresentation.free 📋 Mathlib.Algebra.Module.Presentation.Free
  {A : Type u} [Ring A] {relations : Module.Relations A} (M : Type v) [AddCommGroup M] [Module A M] [IsEmpty relations.R] {solution : relations.Solution M} (h : solution.IsPresentation) : Module.Free A M
• Module.Relations.solutionFinsupp 📋 Mathlib.Algebra.Module.Presentation.Free
  {A : Type u} [Ring A] (relations : Module.Relations A) [IsEmpty relations.R] : relations.Solution (relations.G →₀ A)
• Module.Presentation.tautologicalSolution 📋 Mathlib.Algebra.Module.Presentation.Tautological
  (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (Module.Presentation.tautologicalRelations A M).Solution M
• Module.Presentation.tautologicalRelationsSolutionEquiv 📋 Mathlib.Algebra.Module.Presentation.Tautological
  {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] : (Module.Presentation.tautologicalRelations A M).Solution N ≃ (M →ₗ[A] N)
• Module.Relations.Solution.tensor 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A} (solution₁ : relations₁.Solution M₁) (solution₂ : relations₂.Solution M₂) : (relations₁.tensor relations₂).Solution (TensorProduct A M₁ M₂)
• Module.Relations.Solution.isPresentationCoreTensor 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A} {solution₁ : relations₁.Solution M₁} {solution₂ : relations₂.Solution M₂} (h₁ : solution₁.IsPresentation) (h₂ : solution₂.IsPresentation) : (solution₁.tensor solution₂).IsPresentationCore
• Module.Relations.Solution.IsPresentation.tensor 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A} {solution₁ : relations₁.Solution M₁} {solution₂ : relations₂.Solution M₂} (h₁ : solution₁.IsPresentation) (h₂ : solution₂.IsPresentation) : (solution₁.tensor solution₂).IsPresentation
• Module.Relations.Solution.tensor_var 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Module.Relations A} {relations₂ : Module.Relations A} (solution₁ : relations₁.Solution M₁) (solution₂ : relations₂.Solution M₂) (x✝ : (relations₁.tensor relations₂).G) : (solution₁.tensor solution₂).var x✝ = match x✝ with | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c