smul_mk'

Mathlib.RingTheory.Localization.Defs

URI: https://scilib.ai/kg/mathlib#IsLocalization.smul_mk'

English

For x,y ∈ R and m ∈ M, x • (y/m) equals (x y)/m in the localization.

Русский

Для x,y ∈ R и m ∈ M произведение x умножить на дробь y/m равно дроби (x y)/m в локализации.

LaTeX

$$$x \\cdot mk' S y m = mk' S (x \\cdot y) m$$$

Lean4

theorem smul_mk' (x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m :=
  by
  nth_rw 2 [← one_mul m]
  rw [mk'_mul, mk'_one, Algebra.smul_def]

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

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

Разделы

Аффилиация

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