nontrivial

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

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

English

If 0 ∉ S, then Localization is nontrivial; i.e., N has more than one element.

Русский

Если 0 ∉ S, локализация не тривиальна; то есть в N существует более одного элемента.

LaTeX

$$$0 \\notin S \\Rightarrow \\text{Nontrivial}(N)$$$

Lean4

theorem nontrivial (f : LocalizationMap S N) (h : 0 ∉ S) : Nontrivial N := by
  rwa [← not_subsingleton_iff_nontrivial, f.subsingleton_iff]

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

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

Разделы

Аффилиация

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