NYLL
Module

OpenFiniteIndexSubgroup.lean

Nyll.ClassFieldTheory.Definitions.LocalClassFieldTheory.OpenFiniteIndexSubgroup
1 declaration indexed from sourceView source ↗

Module documentation

Open finite-index subgroups of a field's multiplicative group

Imports2
  • Mathlib.GroupTheory.Index
  • Mathlib.Topology.Algebra.Group.Units
Imported by5

Declarations

abbrev

OpenFiniteIndexSubgroup

L20 ↗
ClassFieldTheory.OpenFiniteIndexSubgroup
Documentation

An open finite-index subgroup of the multiplicative group Kˣ. The inherited order is ordinary subgroup inclusion.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory
universe u
Lean source · statement
abbrev OpenFiniteIndexSubgroup
    (K : Type u) [Field K] [TopologicalSpace K]

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.