instNoZeroDivisorsSubtypeMem

Mathlib.Algebra.Ring.Subring.Defs

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

← MathLib Explorer

English

A subring of a domain has no zero divisors.

Русский

Подкольцо домена не имеет делителей нуля.

LaTeX

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

Lean4

/-- A subring of a ring with no zero divisors has no zero divisors. -/
instance {R} [Ring R] [NoZeroDivisors R] (s : Subring R) : NoZeroDivisors s :=
  s.toSubsemiring.noZeroDivisors

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

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

Разделы

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

Аффилиация

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