2026-05-02 14:29
Mathlib/NumberTheory/MulChar/Duality.lean
feat(NumberTheory/NumberField/Cyclotomic): cardinality of the subgroup of characters associated to an intermediate field equals its degree (#37267) …
Added MulChar.card_subgroupOrderIsoSubgroupMulChar