to_noZeroDivisors

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

In a CancelMonoidWithZero, there are no zero divisors: if ab = 0 then a = 0 or b = 0.

Русский

В CancelMonoidWithZero нулевые делители отсутствуют: если ab = 0, то a = 0 или b = 0.

LaTeX

$$$$ \forall a,b,\ ab = 0 \Rightarrow a = 0 \lor b = 0 $$$$

Lean4

instance (priority := 10) to_noZeroDivisors : NoZeroDivisors M₀ :=
  ⟨fun ab0 => or_iff_not_imp_left.mpr fun ha => mul_left_cancel₀ ha <| ab0.trans (mul_zero _).symm⟩

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

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

Разделы

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

Аффилиация

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