Mostow rigidity | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form and Gopal Prasad, *Strong rigidity of ℚ-rank 1 lattices*, Invent. Math. 21 (1973), 255–286.

Informal solution: Unavailable.

theorem declaration uses `sorry`mostow_rigidity (n : ℕ) (hn : 3 ≤ n) (Γ Λ : Subgroup (LeanEval.Geometry.MostowRigidity.PO n 1))
    (disc_Γ : IsDiscrete (SetLike.coe Γ)) (disc_Λ : IsDiscrete (SetLike.coe Λ))
    [HasFundamentalDomain Γ (LeanEval.Geometry.MostowRigidity.PO n 1)] [HasFundamentalDomain Λ (LeanEval.Geometry.MostowRigidity.PO n 1)]
    (covol_Γ : covolume Γ (LeanEval.Geometry.MostowRigidity.PO n 1) ≠ ⊤) (covol_Λ : covolume Λ (LeanEval.Geometry.MostowRigidity.PO n 1) ≠ ⊤)
    (f : Γ ≃* Λ) : ∃ g : LeanEval.Geometry.MostowRigidity.PO n 1, ∀ γ : Γ, f γ = g * γ * g⁻¹ := byn:ℕhn:3 ≤ nΓ:Subgroup (PO n 1)Λ:Subgroup (PO n 1)disc_Γ:IsDiscrete ↑Γdisc_Λ:IsDiscrete ↑Λinst✝¹:HasFundamentalDomain (↥Γ) (PO n 1) volumeinst✝:HasFundamentalDomain (↥Λ) (PO n 1) volumecovol_Γ:covolume (↥Γ) (PO n 1) volume ≠ ⊤covol_Λ:covolume (↥Λ) (PO n 1) volume ≠ ⊤f:↥Γ ≃* ↥Λ⊢ ∃ g, ∀ (γ : ↥Γ), ↑(f γ) = g * ↑γ * g⁻¹
  sorryAll goals completed! 🐙