left_ne_zero_of_smul

Mathlib.Algebra.GroupWithZero.Action.Defs

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

English

If a • b ≠ 0, then a ≠ 0.

Русский

Если a • b ≠ 0, то a ≠ 0.

LaTeX

$$$\\forall a:\\, M,\\; \\forall b:\\, A,\\; a \\cdot b \\neq 0 \\Rightarrow a \\neq 0$$$

Lean4

theorem left_ne_zero_of_smul : a • b ≠ 0 → a ≠ 0 :=
  mt fun h ↦ smul_eq_zero_of_left h b

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

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

Разделы

Аффилиация

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