natTrailingDegree_eq_support_min'

English

If p ≠ 0, then natTrailingDegree(p) = p.support.min' (nonempty_support_iff.mpr p ≠ 0).

Русский

Если p ≠ 0, то natTrailingDegree(p) равно минимальному элементу p.support, как указано в min' с доказательством не пустоты поддержки.

LaTeX

$$p \neq 0 \Rightarrow \operatorname{natTrailingDegree}(p) = p.support.min'(\text{nonempty_support_iff.mpr } p \neq 0)$$

Lean4

theorem natTrailingDegree_eq_support_min' (h : p ≠ 0) :
    natTrailingDegree p = p.support.min' (nonempty_support_iff.mpr h) := by
  rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]

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