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