isReduced_of_noZeroDivisors

Mathlib.RingTheory.Nilpotent.Defs

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

English

If R has no zero divisors, then R is reduced.

Русский

Если в кольце R нет делителей нуля, то R является редуцированным.

LaTeX

$$[NoZeroDivisors R] ⇒ IsReduced R$$

Lean4

instance (priority := 900) isReduced_of_noZeroDivisors [MonoidWithZero R] [NoZeroDivisors R] : IsReduced R :=
  ⟨fun _ ⟨_, hn⟩ => pow_eq_zero hn⟩

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

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

Разделы

Аффилиация

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