inv_hom_apply

Mathlib.Algebra.Category.Ring.Basic

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

English

For an isomorphism e: R ≅ S and r ∈ R, e.inv (e.hom r) = r.

Русский

Для изоморфизма e: R ≅ S и элемента r ∈ R выполняется e.inv (e.hom r) = r.

LaTeX

$$$ \forall {R S : CommSemiRingCat} (e: R ≅ S) (r: R), e.inv (e.hom r) = r. $$$

Lean4

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

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

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

Разделы

Аффилиация

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