Module

PowerClassGroup.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.PowerClassGroup

2 declarations indexed from sourceView source ↗

Module documentation

Imports2

Imported by5

def

ClassFieldTheory.PowerClassGroup

Documentation

The multiplicative group of a field modulo its n-th powers.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

def PowerClassGroup (K : Type u) [Field K] (n : ℕ+) : Type u

instance

ClassFieldTheory.instCommGroupPowerClassGroup

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

instance instCommGroupPowerClassGroup
    (K : Type u) [Field K] (n : ℕ+) : CommGroup (PowerClassGroup K n)