Commit 2026-05-02 14:29 d9874e42

View on Github →

feat(NumberTheory/NumberField/Cyclotomic): cardinality of the subgroup of characters associated to an intermediate field equals its degree (#37267) New main result : card_intermediateFieldEquivSubgroupChar: the cardinality of the subgroup of Dirichlet characters of level n associated to an intermediate field F of ℚ(ζₙ)/ℚ equals the degree [F : ℚ].

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

added theorem Subgroup.card_mapSubgroup

Modified Mathlib/GroupTheory/FiniteAbelian/Duality.lean

added theorem CommGroup.card_restrictHom_ker

added theorem CommGroup.card_subgroupOrderIsoSubgroupMonoidHom

Modified Mathlib/NumberTheory/MulChar/Duality.lean

added theorem MulChar.card_subgroupOrderIsoSubgroupMulChar

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

added theorem IsCyclotomicExtension.Rat.card_intermediateFieldEquivSubgroupChar

added theorem IsCyclotomicExtension.Rat.card_subgroupGalEquivSubgroupChar