surj

Mathlib.GroupTheory.MonoidLocalization.Basic

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

English

Given a localization map f and z,w in N, there exist z',w' and d ∈ S such that z f d = f z' and w f d = f w'.

Русский

Для любых z,w ∈ N существуют z', w' ∈ M и d ∈ S, такие что z f(d) = f(z') и w f(d) = f(w').

LaTeX

$$$\\exists z',w',d:\\; z\\,f(d) = f(z') \\land w\\,f(d) = f(w').$$$

Lean4

@[to_additive]
theorem surj (f : LocalizationMap S N) (z : N) : ∃ x : M × S, z * f x.2 = f x.1 :=
  f.3 z

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

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

Разделы

Аффилиация

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