Module

PowerClassPow.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.PowerClassPow

1 declaration indexed from sourceView source ↗

Module documentation

The quotient map to power classes preserves powers.

Imports1

Imported by1

theorem

ClassFieldTheory.powerClass_pow

Documentation

The class of a power is the corresponding power of the class.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem powerClass_pow
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ) (m : ℕ) :
    powerClass K n (a ^ m) = (powerClass K n a) ^ m