Theorems · Theorem · commutative algebra

Algebra.Generators.ker_naive

∀ {R : Type u} [inst : CommRing R] {σ : Type u_8} {I : Ideal (MvPolynomial σ R)}
  (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x),
  (Algebra.Generators.naive s hs).ker = I

Defined in

Mathlib.RingTheory.Extension.Generators

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing