Theorems · Theorem · group theory
Fintype.card_units
∀ (α : Type u_1) [inst : GroupWithZero α] [inst_1 : Fintype α] [inst_2 : DecidableEq α], Fintype.card αˣ = Fintype.card α - 1
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Unitsstatement · cited by 2,804
- Fintype.cardstatement and proof · cited by 1,386
- GroupWithZerostatement and proof · cited by 691
- Nat.card_eq_fintype_cardproof · cited by 200
- Nat.card_unitsproof · cited by 6
Cited by9
Results whose statement or proof uses this declaration.
- FiniteField.pow_card_sub_one_eq_oneproof · cited by 7
- Projectivization.cardproof · cited by 3
- ZMod.card_unitsproof · cited by 2
- char_dvd_card_solutions_of_sum_ltproof · cited by 2
- FiniteField.sum_pow_unitsproof · cited by 1
- Fintype.card_eq_card_units_add_oneproof · cited by 1
- MulChar.exists_mulChar_orderOfproof · cited by 1
- MulChar.orderOf_dvd_card_sub_oneproof · cited by 0
- MulChar.exists_mulChar_orderOf_eq_card_unitsproof · cited by 0