mk'_eq_mul_mk'_one

Mathlib.RingTheory.Localization.Defs

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

English

The fraction mk' S x y equals algebraMap_R^S(x) times mk' S 1 y.

Русский

Дробь mk' S x y равна algebraMap_R^S(x) умноженной на mk' S 1 y.

LaTeX

$$$mk' S x y = (algebraMap_R^S x) \\cdot mk' S 1 y$$$

Lean4

theorem mk'_eq_mul_mk'_one (x : R) (y : M) : mk' S x y = (algebraMap R S) x * mk' S 1 y :=
  ((toLocalizationMap M S).mul_mk'_one_eq_mk' _ _).symm

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

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

Разделы

Аффилиация

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