Module

PowerClassMul.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.PowerClassMul

1 declaration indexed from sourceView source ↗

Module documentation

The quotient map to power classes preserves multiplication.

Imports1

Imported by1

theorem

ClassFieldTheory.powerClass_mul

Documentation

The class of a product is the product of the classes.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem powerClass_mul
    (K : Type u) [Field K] (n : ℕ+) (a b : Kˣ) :
    powerClass K n (a * b) = powerClass K n a * powerClass K n b