frobeniusEquiv_symm_comp_frobenius

English

The composition of the inverse Frobenius equivalence with Frobenius equals the identity on R; i.e., (frobeniusEquiv R p).symm ∘ (frobenius R p) = id_R.

Русский

Обратная эквивалентность Фробениуса в сочетании с Фробениусом образует тождество: (frobeniusEquiv R p).symm ∘ (frobenius R p) = id_R.

LaTeX

$$$ (frobeniusEquiv R p).symm \circ frobenius R p = \mathrm{id}_R. $$$

Lean4

@[simp]
theorem frobeniusEquiv_symm_comp_frobenius :
    ((frobeniusEquiv R p).symm : R →+* R).comp (frobenius R p) = RingHom.id R := by ext; simp

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