instance Local_field_is_locally_compact {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : LocallyCompactSpace K

instance Local_field_is_t2 {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : T2Space K

instance Local_field_is_na_add_group {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : NonarchimedeanAddGroup K

instance instTotallySeparatedSpace_padicRep {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TotallySeparatedSpace K

instance local_field_is_totally_disconnected {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TotallyDisconnectedSpace K

@[reducible, inline]

abbrev Mat_padic {K : Type u_1} (n : ℕ) : Type u_1

Equations

• Mat_padic n = Matrix (Fin n) (Fin n) K

@[reducible, inline]

abbrev GL_padic {K : Type u_1} [Field K] (n : ℕ) : Type u_1

Equations

• GL_padic n = GL (Fin n) K

theorem Mat_padic_is_totally_disconnected {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : TotallyDisconnectedSpace (Matrix (Fin n) (Fin n) K)

theorem Mat_padic_is_locally_compact {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : LocallyCompactSpace (Matrix (Fin n) (Fin n) K)

theorem Mat_padic_is_Hausdorff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : T2Space (Matrix (Fin n) (Fin n) K)

theorem GL_padic_is_locally_compact {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : LocallyCompactSpace (GL (Fin n) K)

theorem GL_padic_is_Hausdorff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : T2Space (GL (Fin n) K)

theorem GL_padic_is_totally_disconnected {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : TotallyDisconnectedSpace (GL (Fin n) K)

theorem GL_padic_hasCompactOpenSubgroupBasis {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : HasCompactOpenSubgroupBasis (GL (Fin n) K)