neg_slash — Mathlib

English

For any k, g, a in the additive group, the slash action respects negation: (−a) ∣[k] g = −(a ∣[k] g).

Русский

Для любых k, g и a из группы сложения выполняется: (−a) ∣[k] g = −(a ∣[k] g).

LaTeX

$$$(-a) \lvert[k] g = -(a \lvert[k] g) $$$

Lean4

@[simp]
theorem neg_slash {β G α : Type*} [Monoid G] [AddGroup α] [SlashAction β G α] (k : β) (g : G) (a : α) :
    (-a) ∣[k] g = -a ∣[k] g :=
  eq_neg_of_add_eq_zero_left <| by rw [← add_slash, neg_add_cancel, zero_slash]

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