mem_conjGL' — Mathlib

English

A deprecated form of mem_conjGL expressing the same membership condition in a simplified form.

Русский

Устаревшая форма mem_conjGL, выражающая ту же условность принадлежности в упрощённой форме.

LaTeX

$$$$ \text{mem_conjGL}'(\Gamma, g, x) \iff x \in \text{conjGL}(\Gamma, g). $$$$

Lean4

@[deprecated "use mem_conjGL" (since := "2025-08-16")]
theorem mem_conjGL' {Γ : Subgroup SL(2, ℤ)} {g : GL (Fin 2) ℝ} {x : SL(2, ℤ)} :
    x ∈ conjGL Γ g ↔ ∃ y ∈ Γ, g⁻¹ * y * g = x := by
  rw [mem_conjGL]
  refine exists_congr fun y ↦ and_congr_right fun hy ↦ ?_
  rw [eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul]

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