mul_mul_mul_inv_mem_range_inl — Mathlib

English

For σ, σ' ∈ S.Section and g₁, g₂ ∈ G, the product σ(g₁) · σ(g₂) · (σ(g₁ g₂))⁻¹ lies in S.inl.range.

Русский

Для σ, σ' ∈ S.Section и g₁, g₂ ∈ G произведение σ(g₁) · σ(g₂) · (σ(g₁ g₂))⁻¹ лежит в S.inl.range.

LaTeX

$$$ σ(g_1) \\cdot σ(g_2) \\cdot (σ(g_1 g_2))^{-1} \\in S.inl.range $$$

Lean4

@[to_additive]
theorem mul_mul_mul_inv_mem_range_inl : σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹ ∈ S.inl.range := by
  simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section, mul_inv_cancel]

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