mem_conjGL — Mathlib

English

An element x lies in conjGL(Γ, g) iff there exists y ∈ Γ with y = g x g⁻¹.

Русский

Элемент x принадлежит conjGL(Γ, g) тогда и только тогда, когда существует y ∈ Γ с y = g x g⁻¹.

LaTeX

$$$$ x \in \text{conjGL}(\Gamma, g) \;\Longleftrightarrow\; \exists y \in \Gamma:\; y = g x g^{-1}. $$$$

Lean4

@[simp]
theorem mem_conjGL {Γ : Subgroup SL(2, ℤ)} {g : GL (Fin 2) ℝ} {x : SL(2, ℤ)} :
    x ∈ conjGL Γ g ↔ ∃ y ∈ Γ, y = g * x * g⁻¹ := by
  simp [conjGL, mapGL, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]

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