star_eq_zero — Mathlib

English

Let R be an additive monoid with a star operation (StarAddMonoid). Then for every x in R, star x = 0 if and only if x = 0.

Русский

Пусть R — добавочно-монойд с операцией звезды. Тогда для каждого x в R верно: star x = 0 ⇔ x = 0.

LaTeX

$$$$ \forall x \in R,\ x^{*} = 0 \iff x = 0. $$$$

Lean4

@[simp]
theorem star_eq_zero [AddMonoid R] [StarAddMonoid R] {x : R} : star x = 0 ↔ x = 0 :=
  starAddEquiv.map_eq_zero_iff (M := R)

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