Fermat's Last Theorem in Lean 4

Namespace `RationalLattice` 2 theorems

Covolume of an adelic rational lattice as Haar ratio RationalLattice.abs_det_eq_measure_div_of_squeeze 0 below · cited by 1 · depth 27
Right GL₃ translation scales finite-adelic integrals by inverse idele norm RationalLattice.integral_comp_vecMul_eq_inv_ideleNorm_mul 8 below · cited by 1 · depth 27

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.