mk'_mul_eq_mk'_of_mul

Mathlib.GroupTheory.MonoidLocalization.Basic

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

English

Similarly, swapping the factors gives f.mk' x2 y · f x1 = f.mk' (x1 x2) y.

Русский

Аналогично, поменяв местами множители, выполняется f.mk' x2 y · f x1 = f.mk' (x1 x2) y.

LaTeX

$$$ f.mk' x_2 y \cdot f(x_1) = f.mk' (x_1 x_2) y $$$

Lean4

@[to_additive]
theorem mk'_mul_eq_mk'_of_mul (x₁ x₂) (y : S) : f.mk' x₂ y * f x₁ = f.mk' (x₁ * x₂) y := by
  rw [mul_comm, mul_mk'_eq_mk'_of_mul]

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

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

Разделы

Аффилиация

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