iso_symm_apply

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalizedModule.iso_symm_apply

English

The composition (lift S f g h) ∘ f equals g.

Русский

Составление (lift S f g h) ∘ f равно g.

LaTeX

$$$$ (\mathrm{lift}~S~f~g~h) \circ f = g. $$$$

Lean4

@[simp]
theorem iso_symm_apply (x) : (iso S f).symm (f x) = LocalizedModule.mk x 1 :=
  DFunLike.congr_fun (iso_symm_comp S f) x

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

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

Разделы

Аффилиация

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