mul_mk'_one_eq_mk'

Mathlib.GroupTheory.MonoidLocalization.Basic

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

English

Multiplying f x by the fraction f mk' 1 y yields f mk' x y.

Русский

Умножение f x на дробь f.mk' 1 y дает f.mk' x y.

LaTeX

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

Lean4

@[to_additive]
theorem mul_mk'_one_eq_mk' (x) (y : S) : f x * f.mk' 1 y = f.mk' x y := by rw [mul_mk'_eq_mk'_of_mul, mul_one]

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

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

Разделы

Аффилиация

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