instIsPretransitiveSMul — Mathlib

English

If MulAction.IsPretransitive M X, then MulAction.IsPretransitive M (SeparationQuotient X).

Русский

Если действие M на X предтранситивно, то и на SeparationQuotient X предтранситивно.

LaTeX

$$MulAction.IsPretransitive M (SeparationQuotient X)$$

Lean4

@[to_additive]
instance instIsPretransitiveSMul [MulAction.IsPretransitive M X] : MulAction.IsPretransitive M (SeparationQuotient X)
    where exists_smul_eq := surjective_mk.forall₂.2 fun x y ↦ (MulAction.exists_smul_eq M x y).imp fun _ ↦ congr_arg mk

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