instNontrivialFreeRing

Mathlib.RingTheory.FreeRing

URI: https://scilib.ai/kg/mathlib#instNontrivialFreeRing

English

For any α, FreeRing α is nontrivial (i.e., not the zero ring).

Русский

Для любого α свободное кольцо не тождественно нулю.

LaTeX

$$$\\text{Nontrivial}(\\mathrm{FreeRing}(\\alpha))$$$

Lean4

instance (α : Type u) : Nontrivial (FreeRing α) :=
  inferInstanceAs <| Nontrivial (FreeAbelianGroup _)

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

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

Разделы

Аффилиация

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