ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>NeZero n<GOAL>Fintype.card (DihedralGroup n) = 2 * n
<VAR>n : ℕ<GOAL>Nat.card (DihedralGroup n) = 2 * n
<VAR>n : ℕ<VAR>k : ℕ<GOAL>DihedralGroup.r 1 ^ k = DihedralGroup.r ↑k
<VAR>n : ℕ<GOAL>DihedralGroup.r 1 ^ n = 1
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>DihedralGroup.sr i * DihedralGroup.sr i = 1
<VAR>n : ℕ<VAR>i : ZMod n<GOAL>orderOf (DihedralGroup.sr i) = 2
<VAR>n : ℕ<GOAL>orderOf (DihedralGroup.r 1) = n
<VAR>n : ℕ<VAR>NeZero n<VAR>i : ZMod n<GOAL>orderOf (DihedralGroup.r i) = n / n.gcd i.val
<VAR>n : ℕ<VAR>hn : Odd n<GOAL>∀ (x : { p // Commute p.1 p.2 }), (DihedralGroup.OddCommuteEquiv hn) x = match x with | ⟨(DihedralGroup.sr i, DihedralGroup.r a), property⟩ => Sum.inl i | ⟨(DihedralGroup.r a, DihedralGroup.sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(DihedralGroup.sr i, DihedralGroup.sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(DihedralGroup.r i, DihedralGroup.r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))
<VAR>n : ℕ<VAR>hn : Odd n<GOAL>∀ (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n), (DihedralGroup.OddCommuteEquiv hn).symm x = match x with | Sum.inl i => ⟨(DihedralGroup.sr i, DihedralGroup.r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(DihedralGroup.r 0, DihedralGroup.sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(DihedralGroup.r i, DihedralGroup.r j), ⋯⟩
<VAR>n : ℕ<VAR>hn : Odd n<GOAL>Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
<VAR>α : Type u_2<VAR>Mul α<VAR>a : α<VAR>s t : Set α<GOAL>Doset.doset a s t = Set.image2 (fun x x_1 => x * a * x_1) s t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<VAR>a b : α<GOAL>b ∈ Doset.doset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a : G<GOAL>a ∈ Doset.doset a ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a b : G<VAR>hb : b ∈ Doset.doset a ↑H ↑K<GOAL>Doset.doset b ↑H ↑K = Doset.doset a ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ¬Disjoint (Doset.doset a ↑H ↑K) (Doset.doset b ↑H ↑K)<GOAL>b ∈ Doset.doset a ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ¬Disjoint (Doset.doset a ↑H ↑K) (Doset.doset b ↑H ↑K)<GOAL>Doset.doset a ↑H ↑K = Doset.doset b ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>x y : G<GOAL>(Doset.setoid ↑H ↑K).Rel x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>(Doset.setoid ↑⊥ ↑H).Rel = (QuotientGroup.leftRel H).Rel
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>(Doset.setoid ↑H ↑⊥).Rel = (QuotientGroup.rightRel H).Rel
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a b : G<GOAL>Doset.mk H K a = Doset.mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>q : Doset.Quotient ↑H ↑K<GOAL>Doset.mk H K (Quotient.out' q) = q
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>g : G<GOAL>∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (Doset.mk H K g) = h * g * k
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : Doset.doset a ↑H ↑K = Doset.doset b ↑H ↑K<GOAL>Doset.mk H K a = Doset.mk H K b
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a b : Doset.Quotient ↑H.toSubmonoid ↑K<GOAL>a ≠ b → Disjoint (Doset.doset (Quotient.out' a) ↑H ↑K) (Doset.doset (Quotient.out' b) ↑H ↑K)
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>⋃ q, Doset.quotToDoset H K q = Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a : G<GOAL>⋃ k, MulOpposite.op (a * ↑k) • ↑H = Doset.doset a ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>a : G<GOAL>⋃ h, (↑h * a) • ↑K = Doset.doset a ↑H ↑K
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Doset.Quotient ↑⊥.toSubmonoid ↑H = (G ⧸ H)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Doset.Quotient ↑H.toSubmonoid ↑⊥ = Quotient (QuotientGroup.rightRel H)
<VAR>M : Type u_1<VAR>Mul M<GOAL>commProb M = ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2
<VAR>M : Type u_1<VAR>Mul M<VAR>M' : Type u_2<VAR>Mul M'<GOAL>commProb (M × M') = commProb M * commProb M'
<VAR>α : Type u_2<VAR>i : α → Type u_3<VAR>Fintype α<VAR>(a : α) → Mul (i a)<GOAL>commProb ((a : α) → i a) = ∏ a : α, commProb (i a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>Mul β<GOAL>commProb (α → β) = commProb β ^ Fintype.card α
<VAR>M : Type u_1<VAR>Mul M<VAR>Infinite M<GOAL>commProb M = 0
<VAR>M : Type u_1<VAR>Mul M<VAR>Finite M<VAR>h : Nonempty M<GOAL>0 < commProb M
<VAR>M : Type u_1<VAR>Mul M<VAR>Finite M<GOAL>commProb M ≤ 1
<VAR>M : Type u_1<VAR>Mul M<VAR>Finite M<VAR>h : Nonempty M<GOAL>commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
<VAR>G : Type u_2<VAR>Group G<GOAL>commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
<VAR>G : Type u_2<VAR>Group G<VAR>Finite G<VAR>H : Subgroup G<GOAL>commProb ↥H ≤ commProb G * ↑H.index ^ 2
<VAR>G : Type u_2<VAR>Group G<VAR>Finite G<VAR>H : Subgroup G<VAR>H.Normal<GOAL>commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)
<VAR>G : Type u_2<VAR>Group G<VAR>Finite G<GOAL>(↑(Nat.card ↥(commutator G)))⁻¹ ≤ commProb G
<VAR>n : ℕ<VAR>hn : Odd n<GOAL>commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>n / 2 < n
<VAR>n : ℕ<VAR>h0 : n ≠ 0<VAR>h1 : n ≠ 1<GOAL>n / 4 + 1 < n
<GOAL>DihedralGroup.reciprocalFactors 0 = [0]
<VAR>n : ℕ<VAR>h0 : n ≠ 0<VAR>h2 : Even n<GOAL>DihedralGroup.reciprocalFactors n = 3 :: DihedralGroup.reciprocalFactors (n / 2)
<VAR>n : ℕ<VAR>h1 : n ≠ 1<VAR>h2 : Odd n<GOAL>DihedralGroup.reciprocalFactors n = n % 4 * n :: DihedralGroup.reciprocalFactors (n / 4 + 1)
<VAR>n : ℕ<VAR>l : List ℕ<GOAL>commProb (DihedralGroup.Product (n :: l)) = commProb (DihedralGroup n) * commProb (DihedralGroup.Product l)
<VAR>n : ℕ<GOAL>commProb (DihedralGroup.Product (DihedralGroup.reciprocalFactors n)) = 1 / ↑n
<VAR>α : Type u_1<VAR>rels : Set (FreeGroup α)<GOAL>Subgroup.closure (Set.range PresentedGroup.of) = ⊤
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>f : α → G<VAR>rels : Set (FreeGroup α)<VAR>h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1<GOAL>Subgroup.normalClosure rels ≤ (FreeGroup.lift f).ker
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>f : α → G<VAR>rels : Set (FreeGroup α)<VAR>h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1<VAR>x : FreeGroup α<GOAL>x ∈ Subgroup.normalClosure rels → (FreeGroup.lift f) x = 1
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>f : α → G<VAR>rels : Set (FreeGroup α)<VAR>h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1<VAR>x : α<GOAL>(PresentedGroup.toGroup h) (PresentedGroup.of x) = f x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>f : α → G<VAR>rels : Set (FreeGroup α)<VAR>h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1<VAR>g : PresentedGroup rels →* G<VAR>hg : ∀ (x : α), g (PresentedGroup.of x) = f x<VAR>x : PresentedGroup rels<GOAL>g x = (PresentedGroup.toGroup h) x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>rels : Set (FreeGroup α)<VAR>φ ψ : PresentedGroup rels →* G<VAR>hx : ∀ (x : α), φ (PresentedGroup.of x) = ψ (PresentedGroup.of x)<GOAL>φ = ψ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>x : α<VAR>rels : Set (FreeGroup α)<VAR>e : α ≃ β<GOAL>(PresentedGroup.equivPresentedGroup rels e) (PresentedGroup.of x) = PresentedGroup.of (e x)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>x : β<VAR>rels : Set (FreeGroup α)<VAR>e : α ≃ β<GOAL>(PresentedGroup.equivPresentedGroup rels e).symm (PresentedGroup.of x) = PresentedGroup.of (e.symm x)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>P : AddSubmonoid M<GOAL>P.FG ↔ ∃ S, AddSubmonoid.closure S = P ∧ S.Finite
<VAR>M : Type u_1<VAR>Monoid M<VAR>P : Submonoid M<GOAL>P.FG ↔ ∃ S, Submonoid.closure S = P ∧ S.Finite
<VAR>M : Type u_1<VAR>Monoid M<VAR>P : Submonoid M<GOAL>P.FG ↔ (Submonoid.toAddSubmonoid P).FG
<VAR>N : Type u_2<VAR>AddMonoid N<VAR>P : AddSubmonoid N<GOAL>P.FG ↔ (AddSubmonoid.toSubmonoid P).FG
<VAR>M : Type u_1<VAR>Monoid M<VAR>self : Monoid.FG M<GOAL>⊤.FG
<VAR>N : Type u_2<VAR>AddMonoid N<VAR>self : AddMonoid.FG N<GOAL>⊤.FG
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Monoid.FG M ↔ ⊤.FG
<VAR>N : Type u_2<VAR>AddMonoid N<GOAL>AddMonoid.FG N ↔ ⊤.FG
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Monoid.FG M ↔ ∃ S, Submonoid.closure S = ⊤ ∧ S.Finite
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>AddMonoid.FG M ↔ ∃ S, AddSubmonoid.closure S = ⊤ ∧ S.Finite
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Monoid.FG M ↔ AddMonoid.FG (Additive M)
<VAR>N : Type u_2<VAR>AddMonoid N<GOAL>AddMonoid.FG N ↔ Monoid.FG (Multiplicative N)
<VAR>M : Type u_1<VAR>Monoid M<VAR>M' : Type u_3<VAR>Monoid M'<VAR>P : Submonoid M<VAR>h : P.FG<VAR>e : M →* M'<GOAL>(Submonoid.map e P).FG
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>M' : Type u_3<VAR>AddMonoid M'<VAR>P : AddSubmonoid M<VAR>h : P.FG<VAR>e : M →+ M'<GOAL>(AddSubmonoid.map e P).FG
<VAR>M : Type u_1<VAR>Monoid M<VAR>M' : Type u_3<VAR>Monoid M'<VAR>P : Submonoid M<VAR>e : M →* M'<VAR>he : Function.Injective ⇑e<VAR>h : (Submonoid.map e P).FG<GOAL>P.FG
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>M' : Type u_3<VAR>AddMonoid M'<VAR>P : AddSubmonoid M<VAR>e : M →+ M'<VAR>he : Function.Injective ⇑e<VAR>h : (AddSubmonoid.map e P).FG<GOAL>P.FG
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>N : AddSubmonoid M<GOAL>AddMonoid.FG ↥N ↔ N.FG
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Submonoid M<GOAL>Monoid.FG ↥N ↔ N.FG
<VAR>M : Type u_1<VAR>Monoid M<VAR>M' : Type u_3<VAR>Monoid M'<VAR>Monoid.FG M<VAR>f : M →* M'<VAR>hf : Function.Surjective ⇑f<GOAL>Monoid.FG M'
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>M' : Type u_3<VAR>AddMonoid M'<VAR>AddMonoid.FG M<VAR>f : M →+ M'<VAR>hf : Function.Surjective ⇑f<GOAL>AddMonoid.FG M'
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>r : M<GOAL>(AddSubmonoid.multiples r).FG
<VAR>M : Type u_1<VAR>Monoid M<VAR>r : M<GOAL>(Submonoid.powers r).FG
<VAR>G : Type u_3<VAR>Group G<VAR>P : Subgroup G<GOAL>P.FG ↔ ∃ S, Subgroup.closure S = P ∧ S.Finite
<VAR>G : Type u_3<VAR>AddGroup G<VAR>P : AddSubgroup G<GOAL>P.FG ↔ ∃ S, AddSubgroup.closure S = P ∧ S.Finite
<VAR>G : Type u_3<VAR>AddGroup G<VAR>P : AddSubgroup G<GOAL>P.FG ↔ P.FG
<VAR>G : Type u_3<VAR>Group G<VAR>P : Subgroup G<GOAL>P.FG ↔ P.FG
<VAR>G : Type u_3<VAR>Group G<VAR>P : Subgroup G<GOAL>P.FG ↔ (Subgroup.toAddSubgroup P).FG
<VAR>H : Type u_4<VAR>AddGroup H<VAR>P : AddSubgroup H<GOAL>P.FG ↔ (AddSubgroup.toSubgroup P).FG
<VAR>G : Type u_3<VAR>Group G<VAR>self : Group.FG G<GOAL>⊤.FG
<VAR>H : Type u_4<VAR>AddGroup H<VAR>self : AddGroup.FG H<GOAL>⊤.FG
<VAR>G : Type u_3<VAR>Group G<GOAL>Group.FG G ↔ ⊤.FG
<VAR>H : Type u_4<VAR>AddGroup H<GOAL>AddGroup.FG H ↔ ⊤.FG
<VAR>G : Type u_3<VAR>Group G<GOAL>Group.FG G ↔ ∃ S, Subgroup.closure S = ⊤ ∧ S.Finite
<VAR>G : Type u_3<VAR>AddGroup G<GOAL>AddGroup.FG G ↔ ∃ S, AddSubgroup.closure S = ⊤ ∧ S.Finite
<VAR>G : Type u_3<VAR>Group G<GOAL>Group.FG G ↔ ∃ n S, S.card = n ∧ Subgroup.closure ↑S = ⊤
<VAR>G : Type u_3<VAR>AddGroup G<GOAL>AddGroup.FG G ↔ ∃ n S, S.card = n ∧ AddSubgroup.closure ↑S = ⊤
<VAR>G : Type u_3<VAR>AddGroup G<GOAL>AddGroup.FG G ↔ AddMonoid.FG G
<VAR>G : Type u_3<VAR>Group G<GOAL>Group.FG G ↔ Monoid.FG G
<VAR>G : Type u_3<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>AddGroup.FG ↥H ↔ H.FG
<VAR>G : Type u_3<VAR>Group G<VAR>H : Subgroup G<GOAL>Group.FG ↥H ↔ H.FG
<VAR>G : Type u_3<VAR>Group G<GOAL>Group.FG G ↔ AddGroup.FG (Additive G)
<VAR>H : Type u_4<VAR>AddGroup H<GOAL>AddGroup.FG H ↔ Group.FG (Multiplicative H)
<VAR>G : Type u_3<VAR>AddGroup G<VAR>G' : Type u_5<VAR>AddGroup G'<VAR>hG : AddGroup.FG G<VAR>f : G →+ G'<VAR>hf : Function.Surjective ⇑f<GOAL>AddGroup.FG G'
<VAR>G : Type u_3<VAR>Group G<VAR>G' : Type u_5<VAR>Group G'<VAR>hG : Group.FG G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>Group.FG G'
<VAR>G : Type u_3<VAR>Group G<VAR>h : Group.FG G<GOAL>∃ S, S.card = Group.rank G ∧ Subgroup.closure ↑S = ⊤
<VAR>G : Type u_3<VAR>AddGroup G<VAR>h : AddGroup.FG G<GOAL>∃ S, S.card = AddGroup.rank G ∧ AddSubgroup.closure ↑S = ⊤
<VAR>G : Type u_3<VAR>Group G<VAR>h : Group.FG G<VAR>S : Finset G<VAR>hS : Subgroup.closure ↑S = ⊤<GOAL>Group.rank G ≤ S.card
<VAR>G : Type u_3<VAR>AddGroup G<VAR>h : AddGroup.FG G<VAR>S : Finset G<VAR>hS : AddSubgroup.closure ↑S = ⊤<GOAL>AddGroup.rank G ≤ S.card
<VAR>G : Type u_3<VAR>Group G<VAR>G' : Type u_5<VAR>Group G'<VAR>Group.FG G<VAR>Group.FG G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>Group.rank G' ≤ Group.rank G
<VAR>G : Type u_3<VAR>AddGroup G<VAR>G' : Type u_5<VAR>AddGroup G'<VAR>AddGroup.FG G<VAR>AddGroup.FG G'<VAR>f : G →+ G'<VAR>hf : Function.Surjective ⇑f<GOAL>AddGroup.rank G' ≤ AddGroup.rank G
<VAR>G : Type u_3<VAR>Group G<VAR>G' : Type u_5<VAR>Group G'<VAR>Group.FG G<VAR>f : G →* G'<GOAL>Group.rank ↥f.range ≤ Group.rank G
<VAR>G : Type u_3<VAR>AddGroup G<VAR>G' : Type u_5<VAR>AddGroup G'<VAR>AddGroup.FG G<VAR>f : G →+ G'<GOAL>AddGroup.rank ↥f.range ≤ AddGroup.rank G
<VAR>G : Type u_3<VAR>AddGroup G<VAR>G' : Type u_5<VAR>AddGroup G'<VAR>AddGroup.FG G<VAR>AddGroup.FG G'<VAR>f : G ≃+ G'<GOAL>AddGroup.rank G = AddGroup.rank G'
<VAR>G : Type u_3<VAR>Group G<VAR>G' : Type u_5<VAR>Group G'<VAR>Group.FG G<VAR>Group.FG G'<VAR>f : G ≃* G'<GOAL>Group.rank G = Group.rank G'
<VAR>G : Type u_3<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>AddGroup.FG ↥H<VAR>AddGroup.FG ↥K<VAR>h : H = K<GOAL>AddGroup.rank ↥H = AddGroup.rank ↥K
<VAR>G : Type u_3<VAR>Group G<VAR>H K : Subgroup G<VAR>Group.FG ↥H<VAR>Group.FG ↥K<VAR>h : H = K<GOAL>Group.rank ↥H = Group.rank ↥K
<VAR>G : Type u_3<VAR>Group G<VAR>s : Finset G<GOAL>Group.rank ↥(Subgroup.closure ↑s) ≤ s.card
<VAR>G : Type u_3<VAR>AddGroup G<VAR>s : Finset G<GOAL>AddGroup.rank ↥(AddSubgroup.closure ↑s) ≤ s.card
<VAR>G : Type u_3<VAR>Group G<VAR>s : Set G<VAR>Finite ↑s<GOAL>Group.rank ↥(Subgroup.closure s) ≤ Nat.card ↑s
<VAR>G : Type u_3<VAR>AddGroup G<VAR>s : Set G<VAR>Finite ↑s<GOAL>AddGroup.rank ↥(AddSubgroup.closure s) ≤ Nat.card ↑s
<VAR>n : ℕ<VAR>i j : ZMod (2 * n)<GOAL>QuaternionGroup.a i * QuaternionGroup.a j = QuaternionGroup.a (i + j)
<VAR>n : ℕ<VAR>i j : ZMod (2 * n)<GOAL>QuaternionGroup.a i * QuaternionGroup.xa j = QuaternionGroup.xa (j - i)
<VAR>n : ℕ<VAR>i j : ZMod (2 * n)<GOAL>QuaternionGroup.xa i * QuaternionGroup.a j = QuaternionGroup.xa (i + j)
<VAR>n : ℕ<VAR>i j : ZMod (2 * n)<GOAL>QuaternionGroup.xa i * QuaternionGroup.xa j = QuaternionGroup.a (↑n + j - i)
<VAR>n : ℕ<GOAL>1 = QuaternionGroup.a 0
<VAR>n : ℕ<VAR>NeZero n<GOAL>Fintype.card (QuaternionGroup n) = 4 * n
<VAR>n : ℕ<VAR>k : ℕ<GOAL>QuaternionGroup.a 1 ^ k = QuaternionGroup.a ↑k
<VAR>n : ℕ<GOAL>QuaternionGroup.a 1 ^ (2 * n) = 1
<VAR>n : ℕ<VAR>i : ZMod (2 * n)<GOAL>QuaternionGroup.xa i ^ 2 = QuaternionGroup.a ↑n
<VAR>n : ℕ<VAR>i : ZMod (2 * n)<GOAL>QuaternionGroup.xa i ^ 4 = 1
<VAR>n : ℕ<VAR>NeZero n<VAR>i : ZMod (2 * n)<GOAL>orderOf (QuaternionGroup.xa i) = 4
<VAR>n : ℕ<GOAL>orderOf (QuaternionGroup.a 1) = 2 * n
<VAR>n : ℕ<VAR>NeZero n<VAR>i : ZMod (2 * n)<GOAL>orderOf (QuaternionGroup.a i) = 2 * n / (2 * n).gcd i.val
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G' →* G<VAR>hf : Function.Surjective ⇑f<GOAL>(Subgroup.comap f H).index = H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G' →+ G<VAR>hf : Function.Surjective ⇑f<GOAL>(AddSubgroup.comap f H).index = H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G' →+ G<GOAL>(AddSubgroup.comap f H).index = H.relindex f.range
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G' →* G<GOAL>(Subgroup.comap f H).index = H.relindex f.range
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G' →* G<VAR>K : Subgroup G'<GOAL>(Subgroup.comap f H).relindex K = H.relindex (Subgroup.map f K)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G' →+ G<VAR>K : AddSubgroup G'<GOAL>(AddSubgroup.comap f H).relindex K = H.relindex (AddSubgroup.map f K)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<GOAL>H.relindex K * K.index = H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<GOAL>H.relindex K * K.index = H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<GOAL>K.index ∣ H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<GOAL>K.index ∣ H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H ≤ K<GOAL>H.relindex K ∣ H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H ≤ K<GOAL>H.relindex K ∣ H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hKL : K ≤ L<GOAL>(H.subgroupOf L).relindex (K.subgroupOf L) = H.relindex K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hKL : K ≤ L<GOAL>(H.addSubgroupOf L).relindex (K.addSubgroupOf L) = H.relindex K
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hHK : H ≤ K<VAR>hKL : K ≤ L<GOAL>H.relindex K * K.relindex L = H.relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hHK : H ≤ K<VAR>hKL : K ≤ L<GOAL>H.relindex K * K.relindex L = H.relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>(H ⊓ K).relindex K = H.relindex K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>(H ⊓ K).relindex K = H.relindex K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<GOAL>(H ⊓ K).relindex H = K.relindex H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<GOAL>(H ⊓ K).relindex H = K.relindex H
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<GOAL>H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<GOAL>H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>K.Normal<GOAL>K.relindex (H ⊔ K) = K.relindex H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>K.Normal<GOAL>K.relindex (H ⊔ K) = K.relindex H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>K.Normal<GOAL>K.relindex (K ⊔ H) = K.relindex H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>K.Normal<GOAL>K.relindex (K ⊔ H) = K.relindex H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>H.Normal<GOAL>H.relindex K ∣ H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>H.Normal<GOAL>H.relindex K ∣ H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>L : AddSubgroup G<VAR>hHK : H ≤ K<GOAL>K.relindex L ∣ H.relindex L
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>L : Subgroup G<VAR>hHK : H ≤ K<GOAL>K.relindex L ∣ H.relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.index = 2 ↔ ∃ a, ∀ (b : G), Xor' (b + a ∈ H) (b ∈ H)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.index = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>h : H.index = 2<VAR>a b : G<GOAL>a + b ∈ H ↔ (a ∈ H ↔ b ∈ H)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>h : H.index = 2<VAR>a b : G<GOAL>a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>h : H.index = 2<VAR>a : G<GOAL>a + a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>h : H.index = 2<VAR>a : G<GOAL>a * a ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>h : H.index = 2<VAR>a : G<GOAL>2 • a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>h : H.index = 2<VAR>a : G<GOAL>a ^ 2 ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⊤.index = 1
<VAR>G : Type u_1<VAR>Group G<GOAL>⊤.index = 1
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⊥.index = Nat.card G
<VAR>G : Type u_1<VAR>Group G<GOAL>⊥.index = Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⊤.relindex H = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⊤.relindex H = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.relindex ⊤ = H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.relindex ⊤ = H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>⊥.relindex H = Nat.card ↥H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>⊥.relindex H = Nat.card ↥H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.relindex ⊥ = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.relindex ⊥ = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.relindex H = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.relindex H = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<GOAL>f.ker.index = Nat.card ↑(Set.range ⇑f)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>f : G →+ G'<GOAL>f.ker.index = Nat.card ↑(Set.range ⇑f)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>f : G →+ G'<VAR>K : AddSubgroup G<GOAL>f.ker.relindex K = Nat.card ↑(⇑f '' ↑K)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>K : Subgroup G<GOAL>f.ker.relindex K = Nat.card ↑(⇑f '' ↑K)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>Nat.card ↥H * H.index = Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>Nat.card ↥H * H.index = Nat.card G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>f : G →+ G'<VAR>hf : Function.Surjective ⇑f<GOAL>Nat.card G' ∣ Nat.card G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>Nat.card G' ∣ Nat.card G
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G →* G'<GOAL>(Subgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G →+ G'<GOAL>(AddSubgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>(Subgroup.map f H).index ∣ H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G →+ G'<VAR>hf : Function.Surjective ⇑f<GOAL>(AddSubgroup.map f H).index ∣ H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G →+ G'<VAR>hf : f.ker ≤ H<GOAL>H.index ∣ (AddSubgroup.map f H).index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G →* G'<VAR>hf : f.ker ≤ H<GOAL>H.index ∣ (Subgroup.map f H).index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>f : G →* G'<VAR>hf1 : Function.Surjective ⇑f<VAR>hf2 : f.ker ≤ H<GOAL>(Subgroup.map f H).index = H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>f : G →+ G'<VAR>hf1 : Function.Surjective ⇑f<VAR>hf2 : f.ker ≤ H<GOAL>(AddSubgroup.map f H).index = H.index
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.index = Nat.card (G ⧸ H)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.index = Nat.card (G ⧸ H)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.index * Nat.card ↥H = Nat.card G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.index * Nat.card ↥H = Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.index ∣ Nat.card G
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>H.index ∣ Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hHK : H ≤ K<VAR>hKL : K.relindex L = 0<GOAL>H.relindex L = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hHK : H ≤ K<VAR>hKL : K.relindex L = 0<GOAL>H.relindex L = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hKL : K ≤ L<VAR>hHK : H.relindex K = 0<GOAL>H.relindex L = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hKL : K ≤ L<VAR>hHK : H.relindex K = 0<GOAL>H.relindex L = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H.relindex K = 0<GOAL>H.index = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.relindex K = 0<GOAL>H.index = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hHK : H ≤ K<VAR>hHL : H.relindex L ≠ 0<GOAL>K.relindex L ≤ H.relindex L
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hHK : H ≤ K<VAR>hHL : H.relindex L ≠ 0<GOAL>K.relindex L ≤ H.relindex L
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K L : AddSubgroup G<VAR>hKL : K ≤ L<VAR>hHL : H.relindex L ≠ 0<GOAL>H.relindex K ≤ H.relindex L
<VAR>G : Type u_1<VAR>Group G<VAR>H K L : Subgroup G<VAR>hKL : K ≤ L<VAR>hHL : H.relindex L ≠ 0<GOAL>H.relindex K ≤ H.relindex L