noZeroDivisors

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.noZeroDivisors

← MathLib Explorer

English

If a · b = 0 then a = 0 or b = 0 for cardinals a,b.

Русский

Если a · b = 0, то либо a = 0, либо b = 0, для кардиналов a,b.

LaTeX

$$$a \cdot b = 0 \Rightarrow a = 0 \lor b = 0$$$

Lean4

instance noZeroDivisors : NoZeroDivisors Cardinal.{u} where
  eq_zero_or_eq_zero_of_mul_eq_zero := fun {a b} =>
    inductionOn₂ a b fun α β => by simpa only [mul_def, mk_eq_zero_iff, isEmpty_prod] using id

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

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

Разделы

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

Аффилиация

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