leadingCoeffNth_mono — Mathlib

English

If m ≤ n, then I.leadingCoeffNth m ≤ I.leadingCoeffNth n as subideals of R.

Русский

Если m ≤ n, то I.leadingCoeffNth m ≤ I.leadingCoeffNth n как подидеалы R.

LaTeX

$$$m \\le n \\Rightarrow I.leadingCoeffNth m \\le I.leadingCoeffNth n$$$

Lean4

theorem leadingCoeffNth_mono {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ I.leadingCoeffNth n :=
  by
  intro r hr
  simp only [mem_leadingCoeffNth] at hr ⊢
  rcases hr with ⟨p, hpI, hpdeg, rfl⟩
  refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩
  refine le_trans (degree_mul_le _ _) ?_
  grw [hpdeg, degree_X_pow_le]
  rw [← Nat.cast_add, add_tsub_cancel_of_le H]

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