ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>N : Subgroup G<VAR>Group H<VAR>f : G →* H<VAR>hf : Function.Surjective ⇑f<VAR>hN : N = f.ker<VAR>tN : Monoid.IsTorsion ↥N<GOAL>Monoid.IsTorsion H ↔ Monoid.IsTorsion G
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>AddGroup H<VAR>f : G →+ H<VAR>hf : Function.Surjective ⇑f<VAR>hN : N = f.ker<VAR>tN : AddMonoid.IsTorsion ↥N<GOAL>AddMonoid.IsTorsion H ↔ AddMonoid.IsTorsion G
<VAR>G : Type u_1<VAR>Group G<VAR>h : Monoid.ExponentExists G<GOAL>Monoid.IsTorsion G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>h : AddMonoid.ExponentExists G<GOAL>AddMonoid.IsTorsion G
<VAR>G : Type u_1<VAR>Group G<VAR>tG : Monoid.IsTorsion G<VAR>bounded : (Set.range fun g => orderOf g).Finite<GOAL>Monoid.ExponentExists G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>tG : AddMonoid.IsTorsion G<VAR>bounded : (Set.range fun g => addOrderOf g).Finite<GOAL>AddMonoid.ExponentExists G
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<GOAL>Monoid.IsTorsion G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Finite G<GOAL>AddMonoid.IsTorsion G
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Semiring R<VAR>Module R M<VAR>tR : AddMonoid.IsTorsion R<GOAL>AddMonoid.IsTorsion M
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Ring R<VAR>Finite R<VAR>Module R M<GOAL>AddMonoid.IsTorsion M
<VAR>G : Type u_1<VAR>CommMonoid G<GOAL>Monoid.IsTorsion ↥(CommMonoid.torsion G)
<VAR>G : Type u_1<VAR>AddCommMonoid G<GOAL>AddMonoid.IsTorsion ↥(AddCommMonoid.addTorsion G)
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑(CommMonoid.primaryComponent G p) = {g | ∃ n, orderOf g = p ^ n}
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑(AddCommMonoid.primaryComponent G p) = {g | ∃ n, addOrderOf g = p ^ n}
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>g : ↥(AddCommMonoid.primaryComponent G p)<GOAL>∃ n, addOrderOf g = p ^ n
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>g : ↥(CommMonoid.primaryComponent G p)<GOAL>∃ n, orderOf g = p ^ n
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>p' : ℕ<VAR>hp' : Fact (Nat.Prime p')<VAR>hne : p ≠ p'<GOAL>Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p')
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>p' : ℕ<VAR>hp' : Fact (Nat.Prime p')<VAR>hne : p ≠ p'<GOAL>Disjoint (AddCommMonoid.primaryComponent G p) (AddCommMonoid.primaryComponent G p')
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>tG : AddMonoid.IsTorsion G<GOAL>AddCommMonoid.addTorsion G = ⊤
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>tG : Monoid.IsTorsion G<GOAL>CommMonoid.torsion G = ⊤
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>tG : AddMonoid.IsTorsion G<VAR>a : ↥(AddCommMonoid.addTorsion G)<GOAL>tG.torsionAddEquiv a = ↑((AddEquiv.addSubmonoidCongr ⋯) a)
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>tG : Monoid.IsTorsion G<VAR>a : ↥(CommMonoid.torsion G)<GOAL>tG.torsionMulEquiv a = ↑((MulEquiv.submonoidCongr ⋯) a)
<VAR>G : Type u_1<VAR>AddCommMonoid G<VAR>tG : AddMonoid.IsTorsion G<VAR>a : G<GOAL>tG.torsionAddEquiv.symm a = ⟨↑(AddSubmonoid.topEquiv.symm a), ⋯⟩
<VAR>G : Type u_1<VAR>CommMonoid G<VAR>tG : Monoid.IsTorsion G<VAR>a : G<GOAL>tG.torsionMulEquiv.symm a = ⟨↑(Submonoid.topEquiv.symm a), ⋯⟩
<VAR>G : Type u_1<VAR>CommGroup G<GOAL>CommMonoid.torsion G = (CommGroup.torsion G).toSubmonoid
<VAR>G : Type u_1<VAR>AddCommGroup G<GOAL>AddCommMonoid.addTorsion G = (AddCommGroup.torsion G).toAddSubmonoid
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>g : G<GOAL>g ∈ AddCommGroup.torsion G ↔ IsOfFinAddOrder g
<VAR>G : Type u_1<VAR>CommGroup G<VAR>g : G<GOAL>g ∈ CommGroup.torsion G ↔ IsOfFinOrder g
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑(AddCommGroup.primaryComponent G p) = {g | ∃ n, addOrderOf g = p ^ n}
<VAR>G : Type u_1<VAR>CommGroup G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑(CommGroup.primaryComponent G p) = {g | ∃ n, orderOf g = p ^ n}
<VAR>G : Type u_1<VAR>CommGroup G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>IsPGroup p ↥(CommGroup.primaryComponent G p)
<VAR>G : Type u_1<VAR>AddMonoid G<GOAL>¬AddMonoid.IsTorsionFree G ↔ ∃ g, g ≠ 0 ∧ IsOfFinAddOrder g
<VAR>G : Type u_1<VAR>Monoid G<GOAL>¬Monoid.IsTorsionFree G ↔ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
<VAR>G : Type u_1<VAR>Monoid G<VAR>Subsingleton G<GOAL>Monoid.IsTorsionFree G
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>Subsingleton G<GOAL>AddMonoid.IsTorsionFree G
<VAR>G : Type u_3<VAR>CommGroup G<GOAL>Monoid.IsTorsionFree G ↔ CommGroup.torsion G = ⊥
<VAR>G : Type u_3<VAR>AddCommGroup G<GOAL>AddMonoid.IsTorsionFree G ↔ AddCommGroup.torsion G = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>hN : Nontrivial G<GOAL>Monoid.IsTorsion G → ¬Monoid.IsTorsionFree G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>hN : Nontrivial G<GOAL>AddMonoid.IsTorsion G → ¬AddMonoid.IsTorsionFree G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>hN : Nontrivial G<GOAL>AddMonoid.IsTorsionFree G → ¬AddMonoid.IsTorsion G
<VAR>G : Type u_1<VAR>Group G<VAR>hN : Nontrivial G<GOAL>Monoid.IsTorsionFree G → ¬Monoid.IsTorsion G
<VAR>G : Type u_1<VAR>Group G<VAR>tG : Monoid.IsTorsionFree G<VAR>H : Subgroup G<GOAL>Monoid.IsTorsionFree ↥H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>tG : AddMonoid.IsTorsionFree G<VAR>H : AddSubgroup G<GOAL>AddMonoid.IsTorsionFree ↥H
<VAR>η : Type u_3<VAR>Gs : η → Type u_4<VAR>(i : η) → Group (Gs i)<VAR>tfGs : ∀ (i : η), Monoid.IsTorsionFree (Gs i)<GOAL>Monoid.IsTorsionFree ((i : η) → Gs i)
<VAR>η : Type u_3<VAR>Gs : η → Type u_4<VAR>(i : η) → AddGroup (Gs i)<VAR>tfGs : ∀ (i : η), AddMonoid.IsTorsionFree (Gs i)<GOAL>AddMonoid.IsTorsionFree ((i : η) → Gs i)
<VAR>G : Type u_1<VAR>AddCommGroup G<GOAL>AddMonoid.IsTorsionFree (G ⧸ AddCommGroup.torsion G)
<VAR>G : Type u_1<VAR>CommGroup G<GOAL>Monoid.IsTorsionFree (G ⧸ CommGroup.torsion G)
<VAR>M : Type u_3<VAR>AddMonoid M<GOAL>AddMonoid.IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>AddMonoid.IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G
<VAR>M : Type u_3<VAR>AddMonoid M<VAR>NoZeroSMulDivisors ℕ M<GOAL>AddMonoid.IsTorsionFree M
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype (ConjClasses G)<VAR>Fintype G<VAR>(x : ConjClasses G) → Fintype ↑x.carrier<GOAL>∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<GOAL>∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<GOAL>Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ ConjClasses.noncenter G), Nat.card ↑x.carrier = Nat.card G
<VAR>G : Type u_2<VAR>Group G<VAR>(x : ConjClasses G) → Fintype ↑x.carrier<VAR>Fintype G<VAR>Fintype ↥(Subgroup.center G)<VAR>Fintype ↑(ConjClasses.noncenter G)<GOAL>Fintype.card ↥(Subgroup.center G) + ∑ x ∈ (ConjClasses.noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>Monoid M<VAR>c : Con M<VAR>l : List ι<VAR>f g : ι → M<VAR>h : ∀ x ∈ l, c (f x) (g x)<GOAL>c (List.map f l).prod (List.map g l).prod
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddMonoid M<VAR>c : AddCon M<VAR>l : List ι<VAR>f g : ι → M<VAR>h : ∀ x ∈ l, c (f x) (g x)<GOAL>c (List.map f l).sum (List.map g l).sum
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>c : AddCon M<VAR>s : Multiset ι<VAR>f g : ι → M<VAR>h : ∀ x ∈ s, c (f x) (g x)<GOAL>c (Multiset.map f s).sum (Multiset.map g s).sum
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>c : Con M<VAR>s : Multiset ι<VAR>f g : ι → M<VAR>h : ∀ x ∈ s, c (f x) (g x)<GOAL>c (Multiset.map f s).prod (Multiset.map g s).prod
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>c : Con M<VAR>s : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, c (f i) (g i)<GOAL>c (s.prod f) (s.prod g)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>c : AddCon M<VAR>s : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, c (f i) (g i)<GOAL>c (s.sum f) (s.sum g)
<VAR>X : Type u_1<VAR>x : X<GOAL>Finsupp.toFreeAbelianGroup.comp (Finsupp.singleAddHom x) = (smulAddHom ℤ (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)
<VAR>X : Type u_1<GOAL>FreeAbelianGroup.toFinsupp.comp Finsupp.toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)
<VAR>X : Type u_1<GOAL>Finsupp.toFreeAbelianGroup.comp FreeAbelianGroup.toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
<VAR>X : Type u_2<VAR>x : FreeAbelianGroup X<GOAL>Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x
<VAR>X : Type u_1<VAR>x : X<GOAL>FreeAbelianGroup.toFinsupp (FreeAbelianGroup.of x) = Finsupp.single x 1
<VAR>X : Type u_1<VAR>f : X →₀ ℤ<GOAL>FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f
<VAR>X : Type u_1<VAR>a : X →₀ ℤ<GOAL>(FreeAbelianGroup.equivFinsupp X).symm a = Finsupp.toFreeAbelianGroup a
<VAR>X : Type u_1<VAR>a : FreeAbelianGroup X<GOAL>(FreeAbelianGroup.equivFinsupp X) a = FreeAbelianGroup.toFinsupp a
<VAR>X : Type u_1<VAR>x : X<VAR>a : FreeAbelianGroup X<GOAL>x ∈ a.support ↔ (FreeAbelianGroup.coeff x) a ≠ 0
<VAR>X : Type u_1<VAR>x : X<VAR>a : FreeAbelianGroup X<GOAL>x ∉ a.support ↔ (FreeAbelianGroup.coeff x) a = 0
<VAR>X : Type u_1<GOAL>FreeAbelianGroup.support 0 = ∅
<VAR>X : Type u_1<VAR>x : X<GOAL>(FreeAbelianGroup.of x).support = {x}
<VAR>X : Type u_1<VAR>k : ℤ<VAR>h : k ≠ 0<VAR>a : FreeAbelianGroup X<GOAL>(k • a).support = a.support
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s : Submonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>Localization.mk a₁ a₂ ≤ Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s : AddSubmonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>AddLocalization.mk a₁ a₂ ≤ AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s : AddSubmonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>AddLocalization.mk a₁ a₂ < AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s : Submonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ : ↥s<GOAL>Localization.mk a₁ a₂ < Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s : AddSubmonoid α<VAR>b : ↥s<VAR>a : α<GOAL>(AddLocalization.mkOrderEmbedding b) a = (AddLocalization.addMonoidOf s).mk' a b
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s : Submonoid α<VAR>b : ↥s<VAR>a : α<GOAL>(Localization.mkOrderEmbedding b) a = (Localization.monoidOf s).mk' a b
<VAR>G : Type u_1<VAR>AddGroup G<VAR>self : IsAddKleinFour G<GOAL>AddMonoid.exponent G = 2
<VAR>G : Type u_1<VAR>AddGroup G<VAR>self : IsAddKleinFour G<GOAL>Nat.card G = 4
<VAR>G : Type u_1<VAR>Group G<VAR>self : IsKleinFour G<GOAL>Monoid.exponent G = 2
<VAR>G : Type u_1<VAR>Group G<VAR>self : IsKleinFour G<GOAL>Nat.card G = 4
<VAR>G : Type u_1<VAR>AddGroup G<VAR>Fintype G<VAR>IsAddKleinFour G<GOAL>Fintype.card G = 4
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>IsKleinFour G<GOAL>Fintype.card G = 4
<VAR>G : Type u_1<VAR>AddGroup G<VAR>IsAddKleinFour G<GOAL>¬IsAddCyclic G
<VAR>G : Type u_1<VAR>Group G<VAR>IsKleinFour G<GOAL>¬IsCyclic G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>IsAddKleinFour G<VAR>x : G<GOAL>-x = x
<VAR>G : Type u_1<VAR>Group G<VAR>IsKleinFour G<VAR>x : G<GOAL>x⁻¹ = x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>IsAddKleinFour G<VAR>x : G<GOAL>x + x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>IsKleinFour G<VAR>x : G<GOAL>x * x = 1
<VAR>G : Type u_1<VAR>Group G<VAR>IsKleinFour G<VAR>Fintype G<VAR>DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>{x * y, x, y, 1} = Finset.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>IsAddKleinFour G<VAR>Fintype G<VAR>DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hxy : x ≠ y<GOAL>{x + y, x, y, 0} = Finset.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>IsAddKleinFour G<VAR>x y z : G<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hxy : x ≠ y<VAR>hz : z ≠ 0<VAR>hzx : z ≠ x<VAR>hzy : z ≠ y<GOAL>z = x + y
<VAR>G : Type u_1<VAR>Group G<VAR>IsKleinFour G<VAR>x y z : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<VAR>hz : z ≠ 1<VAR>hzx : z ≠ x<VAR>hzy : z ≠ y<GOAL>z = x * y
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>AddGroup G₁<VAR>AddGroup G₂<VAR>IsAddKleinFour G₁<VAR>IsAddKleinFour G₂<GOAL>Nonempty (G₁ ≃+ G₂)
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>Group G₁<VAR>Group G₂<VAR>IsKleinFour G₁<VAR>IsKleinFour G₂<GOAL>Nonempty (G₁ ≃* G₂)
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con Mᵐᵒᵖ<GOAL>(RelIso.symm Con.orderIsoOp) c = c.unop
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon M<GOAL>AddCon.orderIsoOp c = c.op
<VAR>M : Type u_1<VAR>Add M<VAR>c : AddCon Mᵃᵒᵖ<GOAL>(RelIso.symm AddCon.orderIsoOp) c = c.unop
<VAR>M : Type u_1<VAR>Mul M<VAR>c : Con M<GOAL>Con.orderIsoOp c = c.op
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>CommMonoid M<VAR>S : Submonoid M<VAR>CommMonoid N<VAR>f : S.LocalizationMap N<GOAL>Function.Injective ⇑f.toMap ↔ ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<VAR>AddCommMonoid N<VAR>f : S.LocalizationMap N<GOAL>Function.Injective ⇑f.toMap ↔ ∀ ⦃x : M⦄, x ∈ S → IsAddLeftRegular x
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoidWithZero N<VAR>f : S.LocalizationMap N<VAR>h : 0 ∈ S<GOAL>Subsingleton N
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoidWithZero N<VAR>self : S.LocalizationWithZeroMap N<GOAL>(↑self.toMonoidHom).toFun 0 = 0
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>x : ↥S<GOAL>Localization.mk 0 x = 0
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>p : Type u_4<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d<GOAL>Localization.liftOn 0 f H = f 0 1
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoidWithZero N<VAR>f : S.LocalizationMap N<GOAL>f.toMap (f.sec 0).1 = 0
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoidWithZero N<VAR>f : S.LocalizationWithZeroMap N<VAR>IsLeftCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x<GOAL>IsLeftCancelMulZero N
<VAR>M : Type u_1<VAR>CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>CommMonoidWithZero N<VAR>f : S.LocalizationWithZeroMap N<VAR>IsCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x<GOAL>IsCancelMulZero N
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hp : Fact (Nat.Prime p)<GOAL>IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<VAR>hG : Nat.card G = p ^ n<GOAL>IsPGroup p G
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<GOAL>IsPGroup p ↥⊥
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>Fact (Nat.Prime p)<VAR>Finite G<GOAL>IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>Group H<VAR>ϕ : H →* G<VAR>hϕ : Function.Injective ⇑ϕ<GOAL>IsPGroup p H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>H : Subgroup G<GOAL>IsPGroup p ↥H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>Group H<VAR>ϕ : G →* H<VAR>hϕ : Function.Surjective ⇑ϕ<GOAL>IsPGroup p H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>H : Subgroup G<VAR>H.Normal<GOAL>IsPGroup p (G ⧸ H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>Group H<VAR>ϕ : G ≃* H<GOAL>IsPGroup p H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>n : ℕ<VAR>hn : p.Coprime n<VAR>g : G<GOAL>(orderOf g).Coprime n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>n : ℕ<VAR>hn : p.Coprime n<VAR>g : G<GOAL>(hG.powEquiv hn) g = g ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>n : ℕ<VAR>hn : p.Coprime n<VAR>g : G<GOAL>(hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>H.FiniteIndex<GOAL>∃ n, H.index = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<GOAL>Nat.card G = 1 ∨ p ∣ Nat.card G
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>Finite G<GOAL>Nontrivial G ↔ ∃ n > 0, Nat.card G = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>MulAction G α<VAR>a : α<VAR>Finite ↑(MulAction.orbit G a)<GOAL>∃ n, Nat.card ↑(MulAction.orbit G a) = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>MulAction G α<VAR>Finite α<GOAL>Nat.card α ≡ Nat.card ↑(MulAction.fixedPoints G α) [MOD p]
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>MulAction G α<VAR>hpα : ¬p ∣ Nat.card α<GOAL>(MulAction.fixedPoints G α).Nonempty
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_2<VAR>MulAction G α<VAR>Finite α<VAR>hpα : p ∣ Nat.card α<VAR>a : α<VAR>ha : a ∈ MulAction.fixedPoints G α<GOAL>∃ b ∈ MulAction.fixedPoints G α, a ≠ b
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>Nontrivial G<VAR>Finite G<GOAL>Nontrivial ↥(Subgroup.center G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>Nontrivial G<VAR>Finite G<GOAL>⊥ < Subgroup.center G
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hK : IsPGroup p ↥K<VAR>hHK : H ≤ K<GOAL>IsPGroup p ↥H
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<GOAL>IsPGroup p ↥(H ⊓ K)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hK : IsPGroup p ↥K<GOAL>IsPGroup p ↥(H ⊓ K)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>K : Type u_2<VAR>Group K<VAR>ϕ : G →* K<GOAL>IsPGroup p ↥(Subgroup.map ϕ H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>K : Type u_2<VAR>Group K<VAR>ϕ : K →* G<VAR>hϕ : IsPGroup p ↥ϕ.ker<GOAL>IsPGroup p ↥(Subgroup.comap ϕ H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>K : Type u_2<VAR>Group K<VAR>ϕ : K →* G<VAR>hϕ : Function.Injective ⇑ϕ<GOAL>IsPGroup p ↥ϕ.ker
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>K : Type u_2<VAR>Group K<VAR>ϕ : K →* G<VAR>hϕ : Function.Injective ⇑ϕ<GOAL>IsPGroup p ↥(Subgroup.comap ϕ H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>K : Subgroup G<GOAL>IsPGroup p ↥(Subgroup.comap K.subtype H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>K.Normal<GOAL>IsPGroup p ↥(H ⊔ K)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>H.Normal<GOAL>IsPGroup p ↥(H ⊔ K)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>hHK : H ≤ K.normalizer<GOAL>IsPGroup p ↥(H ⊔ K)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>hK : IsPGroup p ↥K<VAR>hHK : K ≤ H.normalizer<GOAL>IsPGroup p ↥(H ⊔ K)
<VAR>G : Type u_1<VAR>Group G<VAR>G₂ : Type u_2<VAR>Group G₂<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ : Subgroup G<VAR>H₂ : Subgroup G₂<VAR>Finite ↥H₁<VAR>Finite ↥H₂<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<GOAL>(Nat.card ↥H₁).Coprime (Nat.card ↥H₂)
<VAR>G : Type u_1<VAR>Group G<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<GOAL>Disjoint H₁ H₂
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hn : 0 < n<GOAL>∃ k > 0, Nat.card ↥(Subgroup.center G) = p ^ k
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>Fact (Nat.Prime p)<VAR>hG : Nat.card G = p ^ 2<GOAL>IsCyclic (G ⧸ Subgroup.center G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>Group G<VAR>Fact (Nat.Prime p)<VAR>hG : Nat.card G = p ^ 2<VAR>a b : G<GOAL>a * b = b * a
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>h : IsCoatom K<GOAL>frattini G ≤ K
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<GOAL>frattini G ≤ Subgroup.comap φ (frattini H)
<VAR>G : Type u_1<VAR>Group G<VAR>IsCoatomic (Subgroup G)<VAR>K : Subgroup G<VAR>h : K ⊔ frattini G = ⊤<GOAL>K = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>Finite G<GOAL>Group.IsNilpotent ↥(frattini G)
<VAR>G : Type u<VAR>Group G<GOAL>commutator G = ⁅⊤, ⊤⁆
<VAR>G : Type u<VAR>Group G<GOAL>commutator G = Subgroup.closure (commutatorSet G)
<VAR>G : Type u<VAR>Group G<GOAL>commutator G = Subgroup.normalClosure (commutatorSet G)
<VAR>G : Type u<VAR>Group G<VAR>Finite ↑(commutatorSet G)<GOAL>Group.rank ↥(commutator G) ≤ Nat.card ↑(commutatorSet G)
<VAR>G : Type u<VAR>Group G<GOAL>⁅Subgroup.centralizer ↑(commutator G), Subgroup.centralizer ↑(commutator G)⁆ ≤ Subgroup.center G
<VAR>G : Type u<VAR>Group G<VAR>a : G<GOAL>Quot.mk Setoid.r a = Abelianization.of a
<VAR>G : Type u<VAR>Group G<VAR>A : Type v<VAR>CommGroup A<VAR>f : G →* A<GOAL>commutator G ≤ f.ker
<VAR>G : Type u<VAR>Group G<VAR>A : Type v<VAR>CommGroup A<VAR>f : G →* A<VAR>x : G<GOAL>(Abelianization.lift f) (Abelianization.of x) = f x
<VAR>G : Type u<VAR>Group G<VAR>A : Type v<VAR>CommGroup A<VAR>f : G →* A<VAR>φ : Abelianization G →* A<VAR>hφ : ∀ (x : G), φ (Abelianization.of x) = f x<VAR>x : Abelianization G<GOAL>φ x = (Abelianization.lift f) x
<VAR>G : Type u<VAR>Group G<GOAL>Abelianization.lift Abelianization.of = MonoidHom.id (Abelianization G)
<VAR>G : Type u<VAR>Group G<VAR>A : Type v<VAR>Monoid A<VAR>φ ψ : Abelianization G →* A<VAR>h : φ.comp Abelianization.of = ψ.comp Abelianization.of<GOAL>φ = ψ
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>f : G →* H<GOAL>Abelianization.lift (Abelianization.of.comp f) = Abelianization.map f
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>f : G →* H<VAR>x : G<GOAL>(Abelianization.map f) (Abelianization.of x) = Abelianization.of (f x)
<VAR>G : Type u<VAR>Group G<GOAL>Abelianization.map (MonoidHom.id G) = MonoidHom.id (Abelianization G)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>f : G →* H<VAR>I : Type w<VAR>Group I<VAR>g : H →* I<GOAL>(Abelianization.map g).comp (Abelianization.map f) = Abelianization.map (g.comp f)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>f : G →* H<VAR>I : Type w<VAR>Group I<VAR>g : H →* I<VAR>x : Abelianization G<GOAL>(Abelianization.map g) ((Abelianization.map f) x) = (Abelianization.map (g.comp f)) x
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>e : G ≃* H<VAR>x : G<GOAL>e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)
<VAR>G : Type u<VAR>Group G<GOAL>(MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G)
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>e : G ≃* H<GOAL>e.abelianizationCongr.symm = e.symm.abelianizationCongr
<VAR>G : Type u<VAR>Group G<VAR>H : Type v<VAR>Group H<VAR>e : G ≃* H<VAR>I : Type v<VAR>Group I<VAR>e₂ : H ≃* I<GOAL>e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr
<VAR>H : Type u_1<VAR>CommGroup H<VAR>a : Abelianization H<GOAL>Abelianization.equivOfComm.symm a = (Abelianization.lift (MonoidHom.id H)) a
<VAR>H : Type u_1<VAR>CommGroup H<VAR>a : H<GOAL>Abelianization.equivOfComm a = Abelianization.of a
<VAR>G : Type u<VAR>Group G<VAR>Finite ↑(commutatorSet G)<GOAL>Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)
<VAR>G : Type u<VAR>Group G<GOAL>⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G
<VAR>G : Type u<VAR>Group G<GOAL>Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(commutatorSet G)
<VAR>G : Type u<VAR>Group G<GOAL>Nat.card ↥(commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(commutator G)
<VAR>n : ℕ<VAR>i j : ZMod n<GOAL>DihedralGroup.r i * DihedralGroup.r j = DihedralGroup.r (i + j)
<VAR>n : ℕ<VAR>i j : ZMod n<GOAL>DihedralGroup.r i * DihedralGroup.sr j = DihedralGroup.sr (j - i)
<VAR>n : ℕ<VAR>i j : ZMod n<GOAL>DihedralGroup.sr i * DihedralGroup.r j = DihedralGroup.sr (i + j)
<VAR>n : ℕ<VAR>i j : ZMod n<GOAL>DihedralGroup.sr i * DihedralGroup.sr j = DihedralGroup.r (j - i)
<VAR>n : ℕ<GOAL>1 = DihedralGroup.r 0