iterateFrobenius_mul_apply — Mathlib

English

The Frobenius map respects multiplication: frobenius R p (xy) = frobenius R p x · frobenius R p y.

Русский

Фробениус сохраняет произведение: frobenius R p (xy) = frobenius R p x · frobenius R p y.

LaTeX

$$$\frobenius R p (x y) = \frobenius R p x \cdot \frobenius R p y$$$

Lean4

theorem iterateFrobenius_mul_apply : iterateFrobenius R p (m * n) x = (iterateFrobenius R p m)^[n] x := by
  simp_rw [coe_iterateFrobenius, Function.iterate_mul]

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