English
If μ = n for some natural n and i ≤ n, then ψ(i) ≠ 0. In particular, the sequence ψ(i) does not vanish up to the weight n.
Русский
Если вес μ равен некоторому натуральному n и для любого i ≤ n вектор ψ(i) не равен нулю: ψ(i) ≠ 0.
LaTeX
$$$\forall i \in \mathbb{N},\ i \le n \implies \psi(i) \neq 0$$$
Lean4
theorem pow_toEnd_f_ne_zero_of_eq_nat [CharZero R] [NoZeroSMulDivisors R M] {n : ℕ} (hn : μ = n) {i} (hi : i ≤ n) :
(ψ i) ≠ 0 := by
intro H
induction i
· exact P.ne_zero (by simpa using H)
·
next i
IH =>
have : ((i + 1) * (n - i) : ℤ) • (toEnd R L M f ^ i) m = 0 :=
by
have := congr_arg (⁅e, ·⁆) H
simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this
rw [← Int.cast_smul_eq_zsmul R, smul_eq_zero, Int.cast_eq_zero, mul_eq_zero, sub_eq_zero, Nat.cast_inj, ←
@Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_eq_zero] at this
simp only [add_eq_zero, one_ne_zero, and_false, false_or] at this
exact (hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_gt i.lt_succ_self
