nontrivial_of_nonZeroDivisors

Mathlib.RingTheory.OreLocalization.NonZeroDivisors

URI: https://scilib.ai/kg/mathlib#OreLocalization.nontrivial_of_nonZeroDivisors

English

If S ⊆ R⁰ then the localization R[S^{-1}] is nontrivial when R is nontrivial.

Русский

Если S ⊆ R⁰, то локализация R[S^{-1}] не тривиальна при условии, что R тривиальна.

LaTeX

$$(S \le R^0) ⇒ Nontrivial OreLocalization(S,R)$$

Lean4

theorem nontrivial_of_nonZeroDivisors [Nontrivial R] (hS : S ≤ R⁰) : Nontrivial R[S⁻¹] :=
  nontrivial_of_nonZeroDivisorsLeft (hS.trans inf_le_left)

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

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

Разделы

Аффилиация

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