Module

PowerClass.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.PowerClass

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by12

def

ClassFieldTheory.powerClass

Documentation

The canonical class of a nonzero field element modulo 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 powerClass (K : Type u) [Field K] (n : ℕ+) : Kˣ →* PowerClassGroup K n