smul_mk'_one

Mathlib.RingTheory.Localization.Defs

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

English

For x ∈ R and m ∈ M, x • mk' S 1 m equals mk' S x m.

Русский

Для x ∈ R и m ∈ M, x • (1/m) = x/m в локализации.

LaTeX

$$$x \\cdot mk' S 1 m = mk' S x m$$$

Lean4

@[simp]
theorem smul_mk'_one (x : R) (m : M) : x • mk' S 1 m = mk' S x m := by rw [smul_mk', mul_one]

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

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

Разделы

Аффилиация

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