Documentation

LeanPool.OrderPQ.PrimeOrder

LeanPool.OrderPQ.PrimeOrder #

theorem ne_iff_eq_of_or_and_ne {α : Type u_1} {a b c : α} (h1 : a = b ∨ a = c) (h2 : b ≠ c) :

a ≠ b ↔ a = c

theorem IsSimpleGroup.ne_bot_iff_eq_top_of_normal {G : Type u_1} [Group G] [IsSimpleGroup G] {H : Subgroup G} (h : H.Normal) :

H ≠ ⊤ ↔ H = ⊥

theorem IsSimpleAddGroup.ne_bot_iff_eq_top_of_normal {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {H : AddSubgroup G} (h : H.Normal) :

H ≠ ⊤ ↔ H = ⊥

theorem IsSimpleGroup.monoidHom_injective_or_eq_one {G : Type u_1} [Group G] [IsSimpleGroup G] {H : Type u_2} [Group H] (φ : G →* H) :

Function.Injective ⇑φ ∨ φ = 1

theorem IsSimpleAddGroup.addMonoidHom_injective_or_eq_zero {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :

Function.Injective ⇑φ ∨ φ = 0

theorem IsSimpleGroup.monoidHom_ne_one_iff_injective {G : Type u_1} [Group G] [IsSimpleGroup G] {H : Type u_2} [Group H] (φ : G →* H) :

φ ≠ 1 ↔ Function.Injective ⇑φ

theorem IsSimpleAddGroup.addMonoidHom_ne_zero_iff_injective {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :

φ ≠ 0 ↔ Function.Injective ⇑φ

theorem Subgroup.eq_bot_or_eq_top_of_prime_card' {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p) {H : Subgroup G} :

H = ⊥ ∨ H = ⊤

theorem AddSubgroup.eq_bot_or_eq_top_of_prime_card' {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddGroup G] (h : Nat.card G = p) {H : AddSubgroup G} :

H = ⊥ ∨ H = ⊤

theorem IsSimpleGroup.of_prime_card {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p) :

IsSimpleGroup G

theorem IsSimpleAddGroup.of_prime_card {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddGroup G] (h : Nat.card G = p) :

IsSimpleAddGroup G

theorem Subgroup.ne_top_iff_eq_bot_of_prime_card {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p) {H : Subgroup G} :

H ≠ ⊤ ↔ H = ⊥

theorem AddSubgroup.ne_top_iff_eq_bot_of_prime_card {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddGroup G] (h : Nat.card G = p) {H : AddSubgroup G} :

H ≠ ⊤ ↔ H = ⊥

theorem Subgroup.zpowers_eq_top_of_ne_one {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p) {x : G} (hx : x ≠ 1) :

zpowers x = ⊤

theorem AddSubgroup.zmultiples_eq_top_of_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddGroup G] (h : Nat.card G = p) {x : G} (hx : x ≠ 0) :

zmultiples x = ⊤

theorem MonoidHom.end_eq_of_apply_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p) {x : G} (hx : x ≠ 1) (f₁ f₂ : G →* G) (h2 : f₁ x = f₂ x) :

f₁ = f₂

theorem AddMonoidHom.end_eq_of_apply_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddGroup G] (h : Nat.card G = p) {x : G} (hx : x ≠ 0) (f₁ f₂ : G →+ G) (h2 : f₁ x = f₂ x) :

f₁ = f₂

theorem MulAut.eq_of_apply_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p) {x : G} (hx : x ≠ 1) (f₁ f₂ : G ≃* G) (h2 : f₁ x = f₂ x) :

f₁ = f₂

theorem AddAut.eq_of_apply_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [AddGroup G] (h : Nat.card G = p) {x : G} (hx : x ≠ 0) (f₁ f₂ : G ≃+ G) (h2 : f₁ x = f₂ x) :

f₁ = f₂