smul_eq_zero_of_right

Mathlib.Algebra.GroupWithZero.Action.Defs

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

English

If b = 0 in A, then a • b = 0 for any a ∈ M.

Русский

Если b = 0 в A, то для любого a ∈ M выполняется a • b = 0.

LaTeX

$$$\\forall a:\\, M,\\; (b = 0) \\Rightarrow a \\cdot b = 0$$$

Lean4

theorem smul_eq_zero_of_right (a : M) {b : A} (h : b = 0) : a • b = 0 :=
  h.symm ▸ smul_zero a

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

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

Разделы

Аффилиация

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