Theorems · Theorem · group theory

groupCohomology.exists_div_of_norm_eq_one

∀ {K L : Type} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L] [IsGalois K L]
  [IsCyclic Gal(L/K)] {g : Gal(L/K)},
  (∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g) → ∀ {x : L}, (Algebra.norm K) x = 1 → ∃ y, ↑y / g ↑y = x

Hilbert's Theorem 90: given a finite cyclic Galois extension L/K, an element x : L such that N_{L/K}(x) = 1, and a generator g of Gal(L/K), there exists y : Lˣ such that y/g y = x.

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Cited by

1 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFiniteDimensionalIsGaloisIsCyclic