∀ {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