mk'_cancel

Mathlib.Algebra.Module.LocalizedModule.Basic

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

← MathLib Explorer

English

For m ∈ M and s ∈ S, mk' f (s·m) s = f m.

Русский

Для m ∈ M и s ∈ S, дробь mk' f (s·m) s равна f m.

LaTeX

$$$mk' f (s\\cdot m) s = f m$$$

Lean4

@[simp]
theorem mk'_cancel (m : M) (s : S) : mk' f (s • m) s = f m :=
  by
  delta mk'
  rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff,
    OneMemClass.coe_one, mk'_one, one_smul]

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

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

Разделы

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

Аффилиация

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