nontrivial

Mathlib.RingTheory.OreLocalization.NonZeroDivisors

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

English

If R is nontrivial and there is an OreSet R⁰, the localization R[R⁰⁻¹] is nontrivial.

Русский

Если R тривиально и существует Ore множество R⁰, локализация R[R⁰⁻¹] не тривиальна.

LaTeX

$$(Nontrivial(R)) ∧ (OreSet(R⁰)) ⇒ Nontrivial OreLocalization(R⁰, R)$$

Lean4

instance nontrivial : Nontrivial R[R⁰⁻¹] :=
  nontrivial_of_nonZeroDivisors (refl R⁰)

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

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

Разделы

Аффилиация

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