vadd_eq_self_of_mem_zmultiples — Mathlib

English

In additive groups, if x lies in zmultiples y and y fixes a, then x fixes a.

Русский

В аддитивной группе, если x лежит в zmultiples y и y фиксирует a, то и x фиксирует a.

LaTeX

$$x ∈ AddSubgroup.zmultiples y → (y + a) = a → (x + a) = a$$

Lean4

theorem vadd_eq_self_of_mem_zmultiples {G : Type*} [AddGroup G] {x y : G} {α : Type*} [AddAction G α]
    (hx : x ∈ AddSubgroup.zmultiples y) {a : α} (hs : y +ᵥ a = a) : x +ᵥ a = a :=
  @smul_eq_self_of_mem_zpowers (Multiplicative G) _ _ _ α _ hx a hs

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