mul_mk'_eq_mk'_of_mul

Mathlib.RingTheory.Localization.Defs

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

← MathLib Explorer

English

For x,y ∈ R and z ∈ M, the product of the map of x with the fraction y/z equals the fraction (x y)/z.

Русский

Для x,y ∈ R и z ∈ M произведение образа x с дробью y/z равно дроби (x y)/z.

LaTeX

$$$(\\text{algebraMap } x) \\cdot mk' S y z = mk' S (x y) z$$

Lean4

theorem mul_mk'_eq_mk'_of_mul (x y : R) (z : M) : (algebraMap R S) x * mk' S y z = mk' S (x * y) z :=
  (toLocalizationMap M S).mul_mk'_eq_mk'_of_mul _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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