Theorem IsCyclotomicExtension.Rat.card_intermediateFieldEquivSubgroupChar

Modification history

2026-05-02 14:29

Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

feat(NumberTheory/NumberField/Cyclotomic): cardinality of the subgroup of characters associated to an intermediate field equals its degree (#37267) …

Added IsCyclotomicExtension.Rat.card_intermediateFieldEquivSubgroupChar View on Github →