mk'_cancel'

Mathlib.Algebra.Module.LocalizedModule.Basic

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

English

Left smul cancellation: s·mk' f m s = f m.

Русский

Левая исчезновение умножения: s·mk' f m s = f m.

LaTeX

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

Lean4

@[simp]
theorem mk'_cancel' (m : M) (s : S) : s • mk' f m s = f m := by
  rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]

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

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

Разделы

Аффилиация

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