frobenius_mul — Mathlib

English

The Frobenius endomorphism is a multiplicative homomorphism that is compatible with the Frobenius-endowed structure; it preserves multiplication.

Русский

Фробениус-эндоморфизм является мультипликативным гомоморфизмом и сохраняет произведение.

LaTeX

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

Lean4

theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
  map_mul (frobenius R p) x y

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