coeff_p_pow_eq_zero — Mathlib

English

If i ≠ j, the j-th coefficient of p^i is zero.

Русский

Если i ≠ j, j-й коэффициент p^i равен нулю.

LaTeX

$$coeff_p_pow_eq_zero(p, i, j, hj) : ((p : 𝕎 R)^i).coeff j = 0$$

Lean4

theorem coeff_p_pow_eq_zero [CharP R p] {i j : ℕ} (hj : j ≠ i) : ((p : 𝕎 R) ^ i).coeff j = 0 := by
  induction i generalizing j with
  | zero =>
    rw [pow_zero, one_coeff_eq_of_pos]
    exact Nat.pos_of_ne_zero hj
  | succ i hi =>
    rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP]
    cases j
    · rw [verschiebung_coeff_zero, zero_pow hp.out.ne_zero]
    · rw [verschiebung_coeff_succ, hi (ne_of_apply_ne _ hj), zero_pow hp.out.ne_zero]

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