Module

PowerClassInv.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.PowerClassInv

1 declaration indexed from sourceView source ↗

Module documentation

The quotient map to power classes preserves inverses.

Imports1

Imported by1

theorem

ClassFieldTheory.powerClass_inv

Documentation

The class of an inverse is the inverse class.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem powerClass_inv
    (K : Type u) [Field K] (n : ℕ+) (a : Kˣ) :
    powerClass K n a⁻¹ = (powerClass K n a)⁻¹