Theorems · Theorem · group theory
CommGroup.card_restrictHom_ker
Deprecated since 2026-07-19Use CommGroup.card_domRestrictHom_ker instead.
∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
[hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
Nat.card ↥(MonoidHom.domRestrictHom H Mˣ).ker = Nat.card (G ⧸ H)Alias of CommGroup.card_domRestrictHom_ker.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidHomstatement · cited by 3,629
- Subgroupstatement · cited by 3,593
- Finitestatement · cited by 3,029
- Unitsstatement · cited by 2,804
- HasQuotient.Quotientstatement · cited by 2,301
- CommMonoidstatement · cited by 2,264
- CommGroupstatement · cited by 990
- Nat.cardstatement · cited by 844
- MonoidHom.kerstatement · cited by 212
- Monoid.exponentstatement · cited by 128
- HasEnoughRootsOfUnitystatement · cited by 56
- MonoidHom.domRestrictHomstatement · cited by 12
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.