ker_naive — Mathlib

English

The kernel of naive generators is the given ideal I when mapped via s.

Русский

Ядро примитивного набора генераторов совпадает с данным идеалом I после отображения через s.

LaTeX

$$$(\\mathrm{Generators.naive}\\,s\\,hs).ker = I$$$

Lean4

theorem ker_naive {σ : Type*} {I : Ideal (MvPolynomial σ R)} (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R)
    (hs : ∀ x, Ideal.Quotient.mk _ (s x) = x) : (Generators.naive s hs).ker = I :=
  I.mk_ker

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