natDegree_preΨ'_pos — Mathlib

English

If n ∈ ℕ satisfies 2 < n and (n : R) ≠ 0, then (W.preΨ' n).natDegree > 0.

Русский

Если n ∈ ℕ удовлетворяет 2 < n и (n : R) ≠ 0, то (W.preΨ' n).natDegree > 0.

LaTeX

$$(2 < n) \Rightarrow (n : R) ≠ 0 \Rightarrow 0 < (W.preΨ' n).natDegree$$

Lean4

theorem natDegree_preΨ'_pos {n : ℕ} (hn : 2 < n) (h : (n : R) ≠ 0) : 0 < (W.preΨ' n).natDegree :=
  by
  simp_rw [W.natDegree_preΨ' h, Nat.div_pos_iff, zero_lt_two, true_and]
  split_ifs <;> exact Nat.AtLeastTwo.prop.trans <| Nat.sub_le_sub_right (Nat.pow_le_pow_left hn 2) _

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