inv_hom_apply

Mathlib.Algebra.Category.Ring.Basic

URI: https://scilib.ai/kg/mathlib#CommRingCat.inv_hom_apply

English

For an isomorphism e: R ≅ S and any r ∈ R, e.inv (e.hom r) = r; i.e., e.inv ∘ e.hom = id_R.

Русский

Для изоморфизма e: R ≅ S и любого r ∈ R выполняется e.inv (e.hom r) = r; то есть e.inv ∘ e.hom = id_R.

LaTeX

$$$e^{-1}(e(r)) = r \; (r \in R)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru