feat(Geometry): Mostow rigidity, algebraic form

[alreadydone]

No description provided.

[alreadydone]

@kim-em This PR now contains two tasks mostow_rigidity and mostow_rigidity_compact. The workspace for the former was generated successfully, but for the latter it contains several errors: see the ChallengeDeps.lean generated. Most notably, the section Topology is not ended, and variable (p q : ℕ) is dropped, leading to errors. Can you maybe ask Claude to fix these bugs?

(I should have also mentioned that open MeasureTheory is duplicated in Challenge.lean. Moreover, if I don't put mostow_rigidity in a separate namespace LeanEval.Geometry section, Challenge.lean will miss the line open LeanEval.Geometry and report errors like PO doesn't exist.)

Update: Since the bug hasn't been fixed, I have opted to remove the cocompact version to satisfy CI.

[kim-em]

🤖 Codex says:

A few changes are needed before this is ready to merge:

• Please put MatrixSum, pmOneMat, PO, their supporting declarations, and the associated instances in a problem-specific namespace such as LeanEval.Geometry.MostowRigidity. The current generic names and instances land directly in the shared LeanEval.Geometry namespace and risk collisions with future problems. Please name the instances as well.
• Please make existence of fundamental domains explicit for both lattices. In Mathlib, MeasureTheory.covolume is defined to be 0 when no HasFundamentalDomain instance exists, so covolume Γ (PO n 1) ≠ ⊤ alone does not faithfully express finite covolume. Adding the corresponding HasFundamentalDomain hypotheses would close that gap.
• Because the statement allows finite-covolume nonuniform lattices, this is the Mostow–Prasad theorem rather than only the original cocompact form of Mostow rigidity. Please cite Prasad, Strong rigidity of ℚ-rank 1 lattices, Invent. Math. 21 (1973), 255–286, in the file and manifest.
• The standard strong-rigidity conclusion says that the given isomorphism f is induced by conjugation. The current conclusion only says that Γ and Λ are conjugate. Please either strengthen the conclusion to realize f, or clarify that the intentionally weaker isomorphic-iff-conjugate formulation is the benchmark target.

Also please add the missing final newline to the manifest.