iterate_verschiebung_iterate_frobenius

English

If for every index n, either x.coeff n = 0 or y.coeff n = 0, then (x + y).coeff n = x.coeff n + y.coeff n.

Русский

Если для каждого индекса n либо x.coeff n = 0, либо y.coeff n = 0, то (x + y).coeff n = x.coeff n + y.coeff n.

LaTeX

$$$ (x + y).coeff n = x.coeff n + y.coeff n $ при условии $ \forall n, x.coeff n = 0 \lor y.coeff n = 0 $$$

Lean4

theorem iterate_verschiebung_iterate_frobenius (x : 𝕎 R) (n : ℕ) : verschiebung^[n] (frobenius^[n] x) = x * (p ^ n) :=
  by
  rw [← comp_apply (f := verschiebung^[n]), ← Function.Commute.comp_iterate verschiebung_frobenius_comm]
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]

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