ProCGroups.Abelian.exists_surjective_prime_character_finite
A prime divisor of a finite abelian group order gives a cyclic quotient of that order.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.AbelianLean source · statement
theorem exists_surjective_prime_character_finite
{p : ℕ} [Fact p.Prime] {A : Type*} [CommGroup A] [Finite A]
(hp : p ∣ Nat.card A) :
∃ χ : A →* Multiplicative (ZMod p), Function.Surjective χ