inv_hom_apply — Mathlib

English

If e: R ≅ S is an isomorphism, then e.inv ∘ e.hom acts as the identity on R; i.e., e.inv(e.hom(r)) = r for all r ∈ R.

Русский

Если e : R ≅ S является изоморфизмом, то e.inv ∘ e.hom действует как тождественный на R; т.е. e.inv(e.hom(r)) = r для всякого r ∈ R.

LaTeX

$$$ e.inv( e.hom(r) ) = r, \quad r \in R. $$$

Lean4

theorem inv_hom_apply {R S : SemiRingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r := by simp

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