Theorems · Theorem · commutative algebra

Algebra.Presentation.mem_ker_naive

∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R)
  (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
  (i : ι), v i ∈ (Algebra.Presentation.naive s hs).ker

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