eq_zero_of_constant_mem_of_maximal

English

Over a field R, if a constant C x lies in a maximal ideal I of R[X], then x must be 0.

Русский

Над полем R, если константа C x принадлежит максимальному идеалу I в R[X], то x равен 0.

LaTeX

$$$x = 0$ if $C x ∈ I$ and I is maximal in $R[X]$ with R a field$$

Lean4

/-- The only constant in a maximal ideal over a field is `0`. -/
theorem eq_zero_of_constant_mem_of_maximal (hR : IsField R) (I : Ideal R[X]) [hI : I.IsMaximal] (x : R) (hx : C x ∈ I) :
    x = 0 := by
  refine Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)
  obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0
  convert I.mul_mem_left (C y) hx
  rw [← C.map_mul, hR.mul_comm y x, hy, RingHom.map_one]

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