sec_spec

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.sec_spec

English

A symmetric variant of sec_spec asserting dual relations across f(sec z).1 and f(sec z).2.

Русский

Симметричная версия sec_spec, устанавливающая двойные отношения через f(sec z).1 и f(sec z).2.

LaTeX

$$$f((f.sec z).1) = f((f.sec z).2) \\cdot z$$$

Lean4

@[to_additive]
theorem sec_spec {f : LocalizationMap S N} (z : N) : z * f (f.sec z).2 = f (f.sec z).1 :=
  Classical.choose_spec <| f.surj z

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

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

Разделы

Аффилиация

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