NYLL
Module

PrimeOrderHom.lean

Nyll.ProCGroups.FiniteGroups.PrimeOrderHom
2 declarations indexed from sourceView source ↗

Module documentation

Homomorphisms from finite groups of prime order

These elementary group-theoretic facts are shared by the ab-faithfulness criterion and by Galois-theoretic character arguments.

Imports2
  • Mathlib.GroupTheory.Perm.Cycle.Type
  • Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Imported by8

Declarations

theorem

injective_iff_ne_one_of_prime_card

L22 ↗
ProCGroups.FiniteStepSolvableQuotients.injective_iff_ne_one_of_prime_card
Documentation

A homomorphism out of a prime-order group is injective exactly when it is nontrivial.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.FiniteStepSolvableQuotients
universe u v
Lean source · statement
theorem injective_iff_ne_one_of_prime_card
    {B : Type u} {A : Type v} [Group B] [Group A]
    (ρ : B →* A) (hB : Nat.Prime (Nat.card B)) :
    Function.Injective ρ ↔ ρ ≠ 1
theorem

exists_prime_card_subgroup_le_ker_of_not_injective

L50 ↗
ProCGroups.FiniteStepSolvableQuotients.exists_prime_card_subgroup_le_ker_of_not_injective
Documentation

A noninjective homomorphism from a finite group has a prime-order subgroup in its kernel.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.FiniteStepSolvableQuotients
universe u v
Lean source · statement
theorem exists_prime_card_subgroup_le_ker_of_not_injective
    {B : Type u} {A : Type v} [Group B] [Finite B] [Group A]
    (ρ : B →* A) (hρ : ¬ Function.Injective ρ) :
    ∃ C : Subgroup B, Nat.Prime (Nat.card C) ∧ C ≤ ρ.ker

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.