mk'_mul_cancel_left

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.mk'_mul_cancel_left

English

Using commutativity, f.mk'(y x) y = f x.

Русский

С учетом коммутативности, f.mk'(yx) y = f x.

LaTeX

$$$ f.mk'(y \cdot x) y = f(x) $$$

Lean4

@[to_additive]
theorem mk'_mul_cancel_left (x) (y : S) : f.mk' ((y : M) * x) y = f x := by rw [mul_comm, mk'_mul_cancel_right]

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

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

Разделы

Аффилиация

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