ΨSq_ne_zero — Mathlib

English

Let W be a Weierstrass curve over a NoZeroDivisors ring R. If n ∈ Z satisfies (n : R) ≠ 0, then W.ΨSq(n) ≠ 0.

Русский

Пусть W — кривая Вейерштрасса над кольцом R без нулевых делителей. При любом n ∈ Z, для которого (n : R) ≠ 0, полином W.ΨSq(n) не равен нулю.

LaTeX

$$$W.\PsiSq(n) \neq 0$$$

Lean4

theorem ΨSq_ne_zero [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) : W.ΨSq n ≠ 0 :=
  by
  by_cases hn : 1 < n.natAbs
  · exact ne_zero_of_natDegree_gt <| W.natDegree_ΨSq_pos hn h
  · rcases hm : n.natAbs with _ | m
    · push_cast [Int.natAbs_eq_zero.mp hm, ne_self_iff_false] at h
    ·
      rcases Int.natAbs_eq_iff.mp hm with rfl | rfl <;>
            rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn <;>
          push_cast [hn, ΨSq_neg, ΨSq_one] <;>
        exact fun h' => h <| C_injective <| by push_cast [hn, C_neg, C_1, h', neg_zero, C_0]; rfl

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