mem_degreeLE — Mathlib

English

For any R, n, and f ∈ R[X], f lies in degreeLE(R,n) if and only if deg f ≤ n.

Русский

Для любого кольца R, натурального n и многочлена f над R верно: f ∈ degreeLE(R,n) тогда и только тогда, когда deg f ≤ n.

LaTeX

$$$f \in \operatorname{degreeLE}_R(n) \iff \deg f \le n.$$$

Lean4

theorem mem_degreeLE {n : WithBot ℕ} {f : R[X]} : f ∈ degreeLE R n ↔ degree f ≤ n := by
  simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]; rfl

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