English
An element x lies in the leadingCoeff ideal of I iff there exists p ∈ I with p.leadingCoeff = x.
Русский
Элемент x принадлежит I.leadingCoeff тогда и только тогда, когда найдется p ∈ I с p.leadingCoeff = x.
LaTeX
$$$x \\in I.leadingCoeff \\iff \\exists p \\in I, p.leadingCoeff = x$$$
Lean4
theorem mem_leadingCoeff (x) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x :=
by
rw [leadingCoeff, Submodule.mem_iSup_of_directed]
· simp only [mem_leadingCoeffNth]
constructor
· rintro ⟨i, p, hpI, _, rfl⟩
exact ⟨p, hpI, rfl⟩
rintro ⟨p, hpI, rfl⟩
exact ⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩
intro i j
exact ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _), I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩
