Theorem Subgroup.card_mapSubgroup

Modification history

2026-05-02 14:29
Mathlib/Algebra/Group/Subgroup/Finite.lean
feat(NumberTheory/NumberField/Cyclotomic): cardinality of the subgroup of characters associated to an intermediate field equals its degree (#37267) …
Added Subgroup.card_mapSubgroupView on Github →