mul_right_eq_zero

Mathlib.Algebra.GroupWithZero.Units.Basic

URI: https://scilib.ai/kg/mathlib#IsUnit.mul_right_eq_zero

English

If b is a unit, then a · b = 0 iff a = 0.

Русский

Если b единица, то a · b = 0 эквивалентно a = 0.

LaTeX

$$$\forall a,b:\, IsUnit b \Rightarrow (a\cdot b = 0 \iff a = 0)$$$

Lean4

theorem mul_right_eq_zero {a b : M₀} (ha : IsUnit a) : a * b = 0 ↔ b = 0 :=
  let ⟨u, hu⟩ := ha
  hu ▸ u.mul_right_eq_zero

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

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

Разделы

Аффилиация

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