dim_le_degree_of_root — Mathlib

English

Similarly, pb.dim ≤ degree(p) under the assumption aeval pb.gen p = 0 and p ≠ 0.

Русский

Аналогично, при aeval pb.gen p = 0 и p ≠ 0, pb.dim ≤ degree(p).

LaTeX

$$p ≠ 0 ∧ aeval(pb.gen, p) = 0 ⇒ pb.dim ≤ p.degree$$

Lean4

theorem dim_le_degree_of_root (h : PowerBasis A S) {p : A[X]} (ne_zero : p ≠ 0) (root : aeval h.gen p = 0) :
    ↑h.dim ≤ p.degree := by
  rw [degree_eq_natDegree ne_zero]
  exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)

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