frobenius_comm — Mathlib

English

The Frobenius endomorphism commutes with any ring homomorphism: g ∘ frobenius_R_p = frobenius_S_p ∘ g.

Русский

Фробениус-эндоморфизм коммутирует с любым кольцевым гомоморфизмом: g ∘ frobenius_{R,p} = frobenius_{S,p} ∘ g.

LaTeX

$$$g \circ \mathrm{frobenius}_{R,p} = \mathrm{frobenius}_{S,p} \circ g$$$

Lean4

/-- The Frobenius endomorphism commutes with any ring homomorphism. -/
theorem frobenius_comm : g.comp (frobenius R p) = (frobenius S p).comp g :=
  ext <| map_frobenius g p

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