addAction_isPretransitive — Mathlib

English

If an additive action of α on β is pretransitive, then the corresponding additive action on Additive α on β is pretransitive.

Русский

Если над β действует аддитивно с предпереставлением, то аналогичное для Additive α действует предпереставимо на β.

LaTeX

$$$\\text{AddAction.IsPretransitive } α β$ from $\\text{MulAction.IsPretransitive } α β$$$

Lean4

instance addAction_isPretransitive [Monoid α] [MulAction α β] [MulAction.IsPretransitive α β] :
    AddAction.IsPretransitive (Additive α) β :=
  ⟨@MulAction.exists_smul_eq α _ _ _⟩

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