tautologicalSolutionIsPresentationCore

English

Every A-module admits a tautological presentation by generators and relations.

Русский

Каждый A-модуль допускает тавтологическую презентацию генераторами и отношениями.

LaTeX

$$$\\text{tautologicalSolutionIsPresentation}$$$

Lean4

/-- Any `A`-module admits a tautological presentation by generators and relations. -/
noncomputable def tautologicalSolutionIsPresentationCore :
    Relations.Solution.IsPresentationCore.{w} (tautologicalSolution A M)
    where
  desc s := tautologicalRelationsSolutionEquiv s
  postcomp_desc _ := rfl
  postcomp_injective
    h := by
    ext m
    exact Relations.Solution.congr_var h m

Похожие утверждения