iso_mk_one

Mathlib.Algebra.Module.LocalizedModule.Basic

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

English

The isomorphism sends mk(x,1) to f(x).

Русский

Изоморфизм отправляет mk(x,1) в f(x).

LaTeX

$$$$ (\mathrm{iso}~S~f)(\mathrm{LocalizedModule.mk}(x,1)) = f(x). $$$$

Lean4

@[simp]
theorem iso_mk_one (x : M) : (iso S f) (LocalizedModule.mk x 1) = f x := by simp [iso_apply_mk]

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

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

Разделы

Аффилиация

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