isPretransitive_mulOpposite — Mathlib

English

The right regular action of a group on itself is transitive: for any x,y ∈ G there exists g ∈ G with x•g = y (namely g = x⁻¹ y in opposite action).

Русский

Правое регулярное действие группы на самой группе транспитивно: для любых x,y ∈ G существует g ∈ G такое, что x·g = y.

LaTeX

$$$\\exists g \\in G, x \\cdot g = y$ for all x,y ∈ G; explicitly, take $g = x^{-1} y$ in the opposite action.$$

Lean4

/-- The right regular action of a group on itself is transitive. -/
@[to_additive /-- The right regular action of an additive group on itself is transitive. -/
    ]
instance isPretransitive_mulOpposite [Group G] : IsPretransitive Gᵐᵒᵖ G :=
  ⟨fun x y ↦ ⟨.op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩

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