instNontrivialSubtypeMem

Mathlib.Algebra.Ring.Subring.Defs

URI: https://scilib.ai/kg/mathlib#Subring.instNontrivialSubtypeMem

← MathLib Explorer

English

A subring of a nontrivial ring is nontrivial.

Русский

Подкольцо не тривиального кольца тоже не тривиально.

LaTeX

$$$$ \text{Nontrivial}(s) $$$$

Lean4

/-- A subring of a non-trivial ring is non-trivial. -/
instance {R} [Ring R] [Nontrivial R] (s : Subring R) : Nontrivial s :=
  s.toSubsemiring.nontrivial

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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