pow_toEnd_f_eq_zero_of_eq_nat — Mathlib

English

Under the same hypotheses as above, in particular μ = n, the element ψ(n+1) is nonzero.

Русский

При тех же гипотезах, что и выше, в особенности при μ = n, элемент ψ(n+1) ненулевой.

LaTeX

$$$\psi(n+1) \neq 0$$$

Lean4

theorem pow_toEnd_f_eq_zero_of_eq_nat [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] {n : ℕ}
    (hn : μ = n) : (ψ(n + 1)) = 0 := by
  by_contra h
  have : t.HasPrimitiveVectorWith (ψ(n + 1)) (n - 2 * (n + 1) : R) :=
    { ne_zero := h
      lie_h := (P.lie_h_pow_toEnd_f _).trans (by simp [hn])
      lie_e := (P.lie_e_pow_succ_toEnd_f _).trans (by simp [hn]) }
  obtain ⟨m, hm⟩ := this.exists_nat
  have : (n : ℤ) < m + 2 * (n + 1) := by omega
  exact this.ne (Int.cast_injective (α := R) <| by simpa [sub_eq_iff_eq_add] using hm)

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