frobenius_comp_frobeniusEquiv_symm

English

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

Русский

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

LaTeX

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

Lean4

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

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