to_noZeroDivisors

Mathlib.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#IsRightCancelMulZero.to_noZeroDivisors

← MathLib Explorer

English

From MulZeroClass together with IsRightCancelMulZero one derives NoZeroDivisors.

Русский

Из MulZeroClass и IsRightCancelMulZero следует NoZeroDivisors.

LaTeX

$$$\NoZeroDivisors\;\alpha$$$

Lean4

theorem to_noZeroDivisors [MulZeroClass α] [IsRightCancelMulZero α] : NoZeroDivisors α where
  eq_zero_or_eq_zero_of_mul_eq_zero {_ y}
    h := or_iff_not_imp_right.mpr fun ne ↦ mul_right_cancel₀ ne ((zero_mul y).symm ▸ h)

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

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

Разделы

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

Аффилиация

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