mk'_sec

Mathlib.RingTheory.Localization.Defs

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

English

mk' S at the specialization given by z equals z: mk'( (sec M z).1, (sec M z).2 ) = z.

Русский

mk' S применённое к представлению z in Sec возвращает z: mk'( (sec M z).1, (sec M z).2 ) = z.

LaTeX

$$$mk'( (\\operatorname{sec}_M z)_1, (\\operatorname{sec}_M z)_2 ) = z$$

Lean4

@[simp]
theorem mk'_sec (z : S) : mk' S (IsLocalization.sec M z).1 (IsLocalization.sec M z).2 = z :=
  (toLocalizationMap M S).mk'_sec _

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

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

Разделы

Аффилиация

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