We show that GLₙ(𝔸ᶠ) and PGLₙ(𝔸ᶠ) are unimodular.

theorem RestrictedProduct.modularCharacter_eq {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] {C : (i : ι) → Subgroup (G i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [∀ (i : ι), SecondCountableTopology (G i)] [∀ (i : ι), IsTopologicalGroup (G i)] [∀ (i : ι), LocallyCompactSpace (G i)] [Countable ι] (g : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(C i)) Filter.cofinite) : MeasureTheory.Measure.modularCharacter g = ∏ᶠ (i : ι), MeasureTheory.Measure.modularCharacter (g i)

instance RestrictedProduct.isUnimodularGroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] {C : (i : ι) → Subgroup (G i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [∀ (i : ι), SecondCountableTopology (G i)] [Countable ι] [∀ (i : ι), IsUnimodularGroup (G i)] : IsUnimodularGroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(C i)) Filter.cofinite)

instance RestrictedProduct.instIsUnimodularGroupUnitsFiniteAdeleRingRingOfIntegers {K : Type u_3} [Field K] [NumberField K] : IsUnimodularGroup (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)ˣ

instance RestrictedProduct.instSecondCountableTopologyUnits_fLT {M : Type u_3} [Monoid M] [TopologicalSpace M] [SecondCountableTopology M] : SecondCountableTopology Mˣ

instance RestrictedProduct.instIsUnimodularGroupGeneralLinearGroupFiniteAdeleRingRingOfIntegers {K : Type u_3} {n : Type u_4} [Field K] [NumberField K] [Fintype n] [DecidableEq n] : IsUnimodularGroup (GL n (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K))

theorem RestrictedProduct.unitsMap_algebraMap_le_center {R : Type u_3} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] : (Units.map ↑(algebraMap R S)).range ≤ Subgroup.center Sˣ

instance RestrictedProduct.instNormalUnitsRangeMapAlgebraMap_fLT {R : Type u_3} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] : (Units.map ↑(algebraMap R S)).range.Normal

instance RestrictedProduct.instBorelSpaceQuotientSubgroupOfSeparatelyContinuousMulOfPolishSpaceOfIsClosedCoe_fLT {G : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [SeparatelyContinuousMul G] [BorelSpace G] [PolishSpace G] (H : Subgroup G) [IsClosed ↑H] : BorelSpace (G ⧸ H)

instance RestrictedProduct.instSecondCountableTopologyUnits_fLT_1 {M : Type u_3} [Monoid M] [TopologicalSpace M] [SecondCountableTopology M] : SecondCountableTopology Mˣ

theorem RestrictedProduct.Module.FaithfullyFlat.smul_top_eq_top_iff {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R M] {I : Ideal R} : I • ⊤ = ⊤ ↔ I = ⊤

theorem RestrictedProduct.Ideal.map_eq_top_iff {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] {I : Ideal R} : Ideal.map (algebraMap R S) I = ⊤ ↔ I = ⊤

theorem RestrictedProduct.Finsupp.linearCombination_comm {R : Type u_3} {I : Type u_4} [CommSemiring R] (u v : I →₀ R) : (Finsupp.linearCombination R ⇑u) v = (Finsupp.linearCombination R ⇑v) u

theorem RestrictedProduct.Module.Free.exists_comp_linearMap_eq_id (R : Type u_3) (A : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Nontrivial A] : ∃ (f : A →ₗ[R] R), f ∘ₗ Algebra.linearMap R A = LinearMap.id

theorem RestrictedProduct.IsModuleTopology.isClosed_one_of_exists_linearMap (R : Type u_3) (A : Type u_4) [CommRing R] [Ring A] [Algebra R A] (H : ∃ (f : A →ₗ[R] R), f ∘ₗ Algebra.linearMap R A = LinearMap.id) [TopologicalSpace R] [TopologicalSpace A] [IsModuleTopology R A] [T1Space A] : IsClosed ↑1

theorem RestrictedProduct.Submonoid.isClosed_units {M : Type u_3} [TopologicalSpace M] [Monoid M] {U : Submonoid M} (hU : IsClosed ↑U) : IsClosed ↑U.units

theorem RestrictedProduct.Units.range_map {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (f : M →* N) (hf : Function.Injective ⇑f) : (Units.map f).range = (MonoidHom.mrange f).units

theorem RestrictedProduct.isClosed_unitsMap_matrix (n : Type u_3) (R : Type u_4) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T1Space R] [Fintype n] [DecidableEq n] : IsClosed ↑(Units.map ↑(algebraMap R (Matrix n n R))).range

instance RestrictedProduct.instIsUnimodularGroupQuotientGeneralLinearGroupFiniteAdeleRingRingOfIntegersSubgroupUnitsMatrixRangeMapAlgebraMap {K : Type u_3} {n : Type u_4} [Field K] [NumberField K] [Fintype n] [DecidableEq n] : IsUnimodularGroup (GL n (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) ⧸ (Units.map ↑(algebraMap (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (Matrix n n (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)))).range)