Module

IsKummerNorm.lean

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.IsKummerNorm

1 declaration indexed from sourceView source ↗

Module documentation

Norms from Kummer algebras

Imports2

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.KummerAlgebra
Mathlib.RingTheory.Norm.Basic

Imported by4

def

IsKummerNorm

ClassFieldTheory.IsKummerNorm

Documentation

A nonzero element b is a norm from the Kummer algebra K[X] / (X^n - a).

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

def IsKummerNorm
    (K : Type u) [Field K] (n : ℕ+) (a b : Kˣ) : Prop