instNontrivial

Mathlib.RingTheory.Localization.FractionRing

URI: https://scilib.ai/kg/mathlib#FractionRing.instNontrivial

English

If R is nontrivial, then FractionRing R is nontrivial.

Русский

Если R не тривиалось, то FractionRing R также не тривиален.

LaTeX

$$FractionRing.instNontrivial$$

Lean4

instance [Nontrivial R] : Nontrivial (FractionRing R) :=
  inferInstance

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

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

Разделы

Аффилиация

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