Maps congruent to the identity modulo a subgroup #
A map θ : G → G is congruent to the identity modulo a subgroup N when g⁻¹ * θ g ∈ N for
every g, that is when θ g lies in the left coset g N of every g. This file records that the
composite of two such maps is again one.
Main results #
TauCeti.inv_mul_apply_apply_mem: maps congruent to the identity modulo a subgroup compose.
theorem
TauCeti.inv_mul_apply_apply_mem
{G : Type u_1}
[Group G]
{N : Subgroup G}
{θ φ : G → G}
(hθ : ∀ (g : G), g⁻¹ * θ g ∈ N)
(hφ : ∀ (g : G), g⁻¹ * φ g ∈ N)
(g : G)
:
Maps congruent to the identity modulo a subgroup compose. If g⁻¹ * θ g ∈ N and
g⁻¹ * φ g ∈ N for every g, then g⁻¹ * θ (φ g) ∈ N for every g.