smul_eq_zero — Mathlib

English

Let u be a unit and x an element in an additive monoid M with a distributive G-action; then u • x = 0 iff x = 0.

Русский

Пусть u — единица, а x — элемент аддитивного моноида M с действием; тогда u • x = 0 эквивалентно x = 0.

LaTeX

$$$ u \\text{ isUnit} \\Rightarrow (u \\cdot x = 0 \\iff x = 0). $$$

Lean4

@[simp]
theorem smul_eq_zero (hu : IsUnit u) : u • x = 0 ↔ x = 0 :=
  smul_eq_zero_iff_eq hu.unit

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