mk'_one

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalizedModule.mk'_one

← MathLib Explorer

English

For any m, mk' f m 1 = f m.

Русский

Для любого m дробь mk' f m 1 равна f m.

LaTeX

$$$mk' f m (1) = f m$$$

Lean4

@[simp]
theorem mk'_one (m : M) : mk' f m (1 : S) = f m := by
  delta mk'
  rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one, one_smul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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