LeanPool.OrderPQ.Basic

theorem Nat.pow_factorization_dvd {n : ℕ} (hn : n ≠ 0) {p : ℕ} (hp : Prime p) : p ^ n.factorization p ∣ n

theorem Nat.Prime.mem_self_primeFactors {p : ℕ} (hp : Prime p) : p ∈ p.primeFactors

theorem Nat.Prime.mem_self_primeFactorsList {p : ℕ} (hp : Prime p) : p ∈ p.primeFactorsList

theorem exists_monoidHom_ne_one {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (h : p ∣ q - 1) : ∃ (φ : MulZMod p →* MulAut (MulZMod q)), φ ≠ 1

theorem monoidHom_eq_one {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (h : ¬p ∣ q - 1) (φ : MulZMod p →* MulAut (MulZMod q)) : φ = 1

theorem Nat.card_eq_mul_card_fiber {α : Type u_2} {β : Type u_3} (f : α → β) {n : ℕ} (hn : n ≠ 0) (h : ∀ (b : β), Nat.card { a : α // f a = b } = n) : Nat.card α = Nat.card β * n

theorem Subgroup.card_prod_mul_card_meet {G : Type u_1} [Group G] [Finite G] (H K : Subgroup G) : Nat.card ↥H * Nat.card ↥K = Nat.card ↑(↑H * ↑K) * Nat.card ↥(H ⊓ K)

theorem Subgroup.prod_eq_of_inf_eq_bot_and_card {G : Type u_1} [Group G] [Finite G] {H K : Subgroup G} (h1 : H ⊓ K = ⊥) (h2 : Nat.card ↥H * Nat.card ↥K = Nat.card G) : ↑H * ↑K = ⊤

theorem Sylow.exists_of_max_dvd_card (p : ℕ) [hp : Fact (Nat.Prime p)] (G : Type u_1) [Group G] [Finite G] : ∃ (P : Sylow p G), Nat.card ↥↑P = p ^ (Nat.card G).factorization p

theorem Subgroup.meet_eq_bot_of_coprime_card {G : Type u_1} [Group G] {H K : Subgroup G} (h : (Nat.card ↥H).Coprime (Nat.card ↥K)) : H ⊓ K = ⊥

theorem nonempty_mulEquiv_semidirectProduct_of_card_eq_prime_mul_prime {G : Type u_1} [Group G] {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p < q) (h : Nat.card G = p * q) : ∃ (φ : MulZMod p →* MulAut (MulZMod q)), Nonempty (G ≃* MulZMod q ⋊[φ] MulZMod p)

theorem nonempty_mulEquiv_mulZMod_prime_semidirectProduct_mulZMod_prime {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] {φ1 φ2 : MulZMod p →* MulAut (MulZMod q)} (hφ1 : φ1 ≠ 1) (hφ2 : φ2 ≠ 1) : Nonempty (MulZMod q ⋊[φ1] MulZMod p ≃* MulZMod q ⋊[φ2] MulZMod p)

theorem exists_monoidHom_ne_one_and_nonempty_mulEquiv_semidirectProduct {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] {G : Type u_1} [Group G] (hpq : p < q) (h : Nat.card G = p * q) (h' : ¬IsCyclic G) : ∃ (φ : MulZMod p →* MulAut (MulZMod q)), φ ≠ 1 ∧ Nonempty (G ≃* MulZMod q ⋊[φ] MulZMod p)

theorem exists_group_card_eq_prime_mul_prime_and_not_isCyclic {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (h : p ∣ q - 1) : ∃ (G : Type) (x : Group G), Nat.card G = p * q ∧ ¬IsCyclic G

theorem isCyclic_of_card_eq_prime_mul_prime {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] {G : Type u_1} [Group G] (hpq : p < q) (h : ¬p ∣ q - 1) (hG : Nat.card G = p * q) : IsCyclic G

theorem isCyclic_of_card_eq_prime_mul_prime' {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] {G : Type u_1} [Group G] (h1 : Nat.card G = p * q) (h2 : p ≠ q ∧ ¬p ∣ q - 1 ∧ ¬q ∣ p - 1) : IsCyclic G

theorem nonempty_mulEquiv_of_card_eq_prime_mul_prime_of_not_isCyclic' {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p < q) {G1 : Type u_2} [Group G1] (h1 : Nat.card G1 = p * q) (h1' : ¬IsCyclic G1) {G2 : Type u_3} [Group G2] (h2 : Nat.card G2 = p * q) (h2' : ¬IsCyclic G2) : Nonempty (G1 ≃* G2)

theorem nonempty_mulEquiv_prod_of_card_eq_prime_pow_two_of_not_isCyclic {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_2} [Group G] (h : Nat.card G = p ^ 2) (h' : ¬IsCyclic G) : Nonempty (G ≃* MulZMod p × MulZMod p)