CompletedGroupAlgebra.instNonemptyCompletedGroupAlgebraOpenQuotientIndex
The finite quotient index type is nonempty, witnessed by the terminal quotient or canonical base object.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]Lean source · statement
instance instNonemptyCompletedGroupAlgebraOpenQuotientIndex
(R : Type u) [CommRing R] [TopologicalSpace R] :
Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)