mul_mk'_eq_mk'_of_mul

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul

English

In the localization, multiplying the image of x1 by the fraction x2/y yields the fraction (x1x2)/y.

Русский

В локализации умножение образа x1 на дробь x2/y дает дробь (x1x2)/y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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