of_compHom — Mathlib

English

If the M-action is pretransitive, then the N-action obtained through a homomorphism f is also pretransitive.

Русский

Если M-действие предтранситивно, то через гомоморфизм f полученное N-действие также предтранситивно.

LaTeX

$$$\\text{MulAction.IsPretransitive.of_compHom } M N α f : \\text{IsPretransitive } N α$.$$

Lean4

@[to_additive]
theorem of_compHom {M N α : Type*} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N)
    [h :
      letI := compHom α f;
      IsPretransitive M α] :
    IsPretransitive N α :=
  letI := compHom α f;
  h.of_smul_eq f rfl

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