Theorems · Theorem · commutative algebra

Algebra.Presentation.naive_toGenerators

∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : optParam (MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R) (Function.surjInv ⋯))
  (hs :
    autoParam
      (∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
      Algebra.Presentation.naive._auto_1),
  (Algebra.Presentation.naive s hs).toGenerators = Algebra.Generators.naive s hs

Defined in

Mathlib.RingTheory.Extension.Presentation.Basic

Cited by

0 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing