right_ne_zero_of_smul

Mathlib.Algebra.GroupWithZero.Action.Defs

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

English

If a • b ≠ 0 for a ∈ M and b ∈ A, then b ≠ 0.

Русский

Если a • b ≠ 0 для a ∈ M и b ∈ A, то b ≠ 0.

LaTeX

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

Lean4

theorem right_ne_zero_of_smul {a : M} {b : A} : a • b ≠ 0 → b ≠ 0 :=
  mt <| smul_eq_zero_of_right a

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

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

Разделы

Аффилиация

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