English
An element x lies in I.leadingCoeffNth n iff there exists p ∈ I with degree p ≤ n and leadingCoeff p = x.
Русский
Элемент x принадлежит I.leadingCoeffNth n тогда и только тогда, когда существует p ∈ I с deg p ≤ n и leadingCoeff p = x.
LaTeX
$$$x \\in I.leadingCoeffNth n \\iff \\exists p \\in I, \\deg p \\le n \\land p.leadingCoeff = x$$$
Lean4
theorem mem_leadingCoeffNth (n : ℕ) (x) : x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, degree p ≤ n ∧ p.leadingCoeff = x :=
by
simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf, mem_degreeLE]
constructor
· rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩
rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg
· refine ⟨0, I.zero_mem, bot_le, ?_⟩
rw [leadingCoeff_zero, eq_comm]
exact coeff_eq_zero_of_degree_lt hpdeg
· refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
· rintro ⟨p, hpI, hpdeg, rfl⟩
have : natDegree p + (n - natDegree p) = n := add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
· apply le_trans (degree_mul_le _ _) _
apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
rw [← Nat.cast_add, this]
· rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]
