NYLL
Module

PowerClassEqOneIff.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.PowerClassEqOneIff
1 declaration indexed from sourceView source ↗

Module documentation

Power-class laws and representatives

For a field K and a positive integer n, PowerClassGroup K n is the quotient of Kˣ by the subgroup of n-th powers. A class is the identity exactly when its representative belongs to the power subgroup.

Imports1
Imported by1

Declarations

theorem

powerClass_eq_one_iff

L24 ↗
ClassFieldTheory.powerClass_eq_one_iff
Documentation

A power class is trivial exactly when its representative is an n-th power.

Source context 2 commands

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

namespace ClassFieldTheory
universe u
Lean source · statement
theorem powerClass_eq_one_iff
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ) :
    powerClass K n a = 1 ↔
      a ∈ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range

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