ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H' H : AddSubgroup G<VAR>h : H' ≤ H<GOAL>∃ S, ↑H' + S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>x : ↑S × ↑T<GOAL>hST.equiv.symm x = ↑x.1 * ↑x.2
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<GOAL>↑(hST.equiv g).1 * ↑(hST.equiv g).2 = g
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<GOAL>↑(hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<GOAL>↑(hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>S : Set G<VAR>hSK : Subgroup.IsComplement S ↑K<VAR>g₁ g₂ : G<GOAL>(hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>T : Set G<VAR>hHT : Subgroup.IsComplement (↑H) T<VAR>g₁ g₂ : G<GOAL>(hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ RightCosetEquivalence (↑H) g₁ g₂
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>S : Set G<VAR>hSK : Subgroup.IsComplement S ↑K<VAR>g : G<GOAL>LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>T : Set G<VAR>hHT : Subgroup.IsComplement (↑H) T<VAR>g : G<GOAL>RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ T<VAR>hg : g ∈ S<GOAL>(hST.equiv g).1 = ⟨g, hg⟩
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ S<VAR>hg : g ∈ T<GOAL>(hST.equiv g).2 = ⟨g, hg⟩
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ T<VAR>hg : g ∈ S<GOAL>(hST.equiv g).2 = ⟨1, h1⟩
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ S<VAR>hg : g ∈ T<GOAL>(hST.equiv g).1 = ⟨1, h1⟩
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>S : Set G<VAR>hSK : Subgroup.IsComplement S ↑K<VAR>g : G<VAR>k : ↥K<GOAL>hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>S : Set G<VAR>hSK : Subgroup.IsComplement S ↑K<VAR>g k : G<VAR>h : k ∈ K<GOAL>hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * ⟨k, h⟩)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>T : Set G<VAR>hHT : Subgroup.IsComplement (↑H) T<VAR>h : ↥H<VAR>g : G<GOAL>hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>T : Set G<VAR>hHT : Subgroup.IsComplement (↑H) T<VAR>h g : G<VAR>hh : h ∈ H<GOAL>hHT.equiv (h * g) = (⟨h, hh⟩ * (hHT.equiv g).1, (hHT.equiv g).2)
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>hs1 : 1 ∈ S<VAR>ht1 : 1 ∈ T<GOAL>hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ T<GOAL>↑(hST.equiv g).1 = g ↔ g ∈ S
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ S<GOAL>↑(hST.equiv g).2 = g ↔ g ∈ T
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ S<GOAL>↑(hST.equiv g).1 = 1 ↔ g ∈ T
<VAR>G : Type u_1<VAR>Group G<VAR>S T : Set G<VAR>hST : Subgroup.IsComplement S T<VAR>g : G<VAR>h1 : 1 ∈ T<GOAL>↑(hST.equiv g).2 = 1 ↔ g ∈ S
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>h : S ∈ Subgroup.leftTransversals ↑H<GOAL>Finite ↑S ↔ H.FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>h : S ∈ AddSubgroup.leftTransversals ↑H<GOAL>Finite ↑S ↔ H.FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>hS : S ∈ AddSubgroup.leftTransversals ↑H<VAR>q : G ⧸ H<GOAL>Quotient.mk'' ↑((AddSubgroup.MemLeftTransversals.toEquiv hS) q) = q
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>hS : S ∈ Subgroup.leftTransversals ↑H<VAR>q : G ⧸ H<GOAL>Quotient.mk'' ↑((Subgroup.MemLeftTransversals.toEquiv hS) q) = q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<VAR>q : G ⧸ H<GOAL>↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) = f q
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<VAR>q : G ⧸ H<GOAL>↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = f q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>hS : S ∈ AddSubgroup.leftTransversals ↑H<VAR>g : G<GOAL>-↑(AddSubgroup.MemLeftTransversals.toFun hS g) + g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>hS : S ∈ Subgroup.leftTransversals ↑H<VAR>g : G<GOAL>(↑(Subgroup.MemLeftTransversals.toFun hS g))⁻¹ * g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>hS : S ∈ Subgroup.leftTransversals ↑H<VAR>g : G<GOAL>g⁻¹ * ↑(Subgroup.MemLeftTransversals.toFun hS g) ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>hS : S ∈ AddSubgroup.leftTransversals ↑H<VAR>g : G<GOAL>-g + ↑(AddSubgroup.MemLeftTransversals.toFun hS g) ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>h : S ∈ Subgroup.rightTransversals ↑H<GOAL>Finite ↑S ↔ H.FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>h : S ∈ AddSubgroup.rightTransversals ↑H<GOAL>Finite ↑S ↔ H.FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>hS : S ∈ AddSubgroup.rightTransversals ↑H<VAR>q : Quotient (QuotientAddGroup.rightRel H)<GOAL>Quotient.mk'' ↑((AddSubgroup.MemRightTransversals.toEquiv hS) q) = q
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>hS : S ∈ Subgroup.rightTransversals ↑H<VAR>q : Quotient (QuotientGroup.rightRel H)<GOAL>Quotient.mk'' ↑((Subgroup.MemRightTransversals.toEquiv hS) q) = q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>f : Quotient (QuotientAddGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q<VAR>q : Quotient (QuotientAddGroup.rightRel H)<GOAL>↑((AddSubgroup.MemRightTransversals.toEquiv ⋯) q) = f q
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>f : Quotient (QuotientGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q<VAR>q : Quotient (QuotientGroup.rightRel H)<GOAL>↑((Subgroup.MemRightTransversals.toEquiv ⋯) q) = f q
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>hS : S ∈ AddSubgroup.rightTransversals ↑H<VAR>g : G<GOAL>g + -↑(AddSubgroup.MemRightTransversals.toFun hS g) ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>hS : S ∈ Subgroup.rightTransversals ↑H<VAR>g : G<GOAL>g * (↑(Subgroup.MemRightTransversals.toFun hS g))⁻¹ ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>S : Set G<VAR>hS : S ∈ AddSubgroup.rightTransversals ↑H<VAR>g : G<GOAL>↑(AddSubgroup.MemRightTransversals.toFun hS g) + -g ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>S : Set G<VAR>hS : S ∈ Subgroup.rightTransversals ↑H<VAR>g : G<GOAL>↑(Subgroup.MemRightTransversals.toFun hS g) * g⁻¹ ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>F : Type u_2<VAR>Group F<VAR>MulAction F G<VAR>MulAction.QuotientAction F H<VAR>f : F<VAR>T : ↑(Subgroup.leftTransversals ↑H)<VAR>g : G<GOAL>f • ↑(Subgroup.MemLeftTransversals.toFun ⋯ g) = ↑(Subgroup.MemLeftTransversals.toFun ⋯ (f • g))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>F : Type u_2<VAR>AddGroup F<VAR>AddAction F G<VAR>AddAction.QuotientAction F H<VAR>f : F<VAR>T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>g : G<GOAL>f +ᵥ ↑(AddSubgroup.MemLeftTransversals.toFun ⋯ g) = ↑(AddSubgroup.MemLeftTransversals.toFun ⋯ (f +ᵥ g))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>F : Type u_2<VAR>AddGroup F<VAR>AddAction F G<VAR>AddAction.QuotientAction F H<VAR>f : F<VAR>T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>q : G ⧸ H<GOAL>f +ᵥ ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) = ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) (f +ᵥ q))
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>F : Type u_2<VAR>Group F<VAR>MulAction F G<VAR>MulAction.QuotientAction F H<VAR>f : F<VAR>T : ↑(Subgroup.leftTransversals ↑H)<VAR>q : G ⧸ H<GOAL>f • ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (f • q))
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>F : Type u_2<VAR>Group F<VAR>MulAction F G<VAR>MulAction.QuotientAction F H<VAR>f : F<VAR>T : ↑(Subgroup.leftTransversals ↑H)<VAR>q : G ⧸ H<GOAL>↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = f • ↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (f⁻¹ • q))
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>F : Type u_2<VAR>AddGroup F<VAR>AddAction F G<VAR>AddAction.QuotientAction F H<VAR>f : F<VAR>T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>q : G ⧸ H<GOAL>↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) q) = f +ᵥ ↑((AddSubgroup.MemLeftTransversals.toEquiv ⋯) (-f +ᵥ q))
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.IsComplement' K<GOAL>IsCompl H K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.IsComplement' K<GOAL>H ⊔ K = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.IsComplement' K<GOAL>Disjoint H K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.IsComplement' K<GOAL>K.index = Nat.card ↥H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H.IsComplement' K<GOAL>Nat.card ↥H * Nat.card ↥K = Nat.card G
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h1 : Disjoint H K<VAR>h2 : ↑H * ↑K = Set.univ<GOAL>H.IsComplement' K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>Finite G<VAR>h1 : Nat.card ↥H * Nat.card ↥K = Nat.card G<VAR>h2 : Disjoint H K<GOAL>H.IsComplement' K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>Finite G<GOAL>H.IsComplement' K ↔ Nat.card ↥H * Nat.card ↥K = Nat.card G ∧ Disjoint H K
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>Finite G<VAR>h1 : Nat.card ↥H * Nat.card ↥K = Nat.card G<VAR>h2 : (Nat.card ↥H).Coprime (Nat.card ↥K)<GOAL>H.IsComplement' K
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>α : Type u_2<VAR>MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<GOAL>H.IsComplement' (MulAction.stabilizer G a)
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)<VAR>k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out' q))<GOAL>(H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out' q
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)<VAR>k : ℤ<GOAL>(H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out' q) = ⟨q, ↑k⟩
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : G ⧸ H<GOAL>H.transferFunction g q = g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out' (Quotient.out' ((H.quotientEquivSigmaZMod g) q).fst)
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : G ⧸ H<GOAL>↑(H.transferFunction g q) = q
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : G ⧸ H<GOAL>H.transferFunction g q ∈ H.transferSet g
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : G ⧸ H<GOAL>↑((Subgroup.MemLeftTransversals.toEquiv ⋯) q) = H.transferFunction g q
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)<VAR>k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out' q))<GOAL>↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (g ^ k.cast • Quotient.out' q)) = g ^ k.cast * Quotient.out' (Quotient.out' q)
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)<VAR>k : ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out' q))<GOAL>↑((Subgroup.MemLeftTransversals.toEquiv ⋯) (g ^ k.cast • Quotient.out' q)) = if k = 0 then g ^ Function.minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q) else g ^ k.cast * Quotient.out' (Quotient.out' q)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>g : (Equiv.Perm α)ᵈᵐᵃ<GOAL>g ∈ MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f ↔ f ∘ ⇑(DomMulAct.mk.symm g) = f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>g : (i : ι) → Equiv.Perm { a // f a = i }<VAR>a : α<VAR>i : ι<VAR>h : f a = i<GOAL>DomMulAct.stabilizerEquiv_invFun g a = ↑((g i) ⟨a, h⟩)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>g : (i : ι) → Equiv.Perm { a // f a = i }<VAR>a : α<GOAL>f (DomMulAct.stabilizerEquiv_invFun g a) = f a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>g : (↥(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f))ᵐᵒᵖ<VAR>a : α<VAR>i : ι<VAR>h : f a = i<GOAL>↑(((DomMulAct.stabilizerMulEquiv f) g i) ⟨a, h⟩) = (DomMulAct.mk.symm ↑(MulOpposite.unop g)) a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : α → ι<VAR>Fintype α<VAR>Fintype ι<VAR>DecidableEq α<VAR>DecidableEq ι<GOAL>Fintype.card { g // f ∘ ⇑g = f } = ∏ i : ι, (Fintype.card { a // f a = i }).factorial
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ n ω, ω.length = n ∧ cs.wordProd ω = w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.length (cs.wordProd ω) ≤ ω.length
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>cs.length 1 = 0
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.length w = 0 ↔ w = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.length w⁻¹ = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>max (cs.length w₁ - cs.length w₂) (cs.length w₂ - cs.length w₁) ≤ cs.length (w₁ * w₂)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>⇑cs.lengthParity ∘ cs.simple = fun x => Multiplicative.ofAdd 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.length (cs.simple i) = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.length w = 1 ↔ ∃ i, w = cs.simple i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (w * cs.simple i) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.IsReduced ω.reverse ↔ cs.IsReduced ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<GOAL>cs.IsReduced (List.take j ω) ∧ cs.IsReduced (List.drop j ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<GOAL>cs.IsReduced (List.take j ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : cs.IsReduced ω<VAR>j : ℕ<GOAL>cs.IsReduced (List.drop j ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>hM : M.M i i' ≠ 0<VAR>hm : m > M.M i i'<GOAL>¬cs.IsReduced (CoxeterSystem.alternatingWord i i' m)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>¬cs.IsLeftDescent 1 i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>¬cs.IsRightDescent 1 i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsLeftDescent w⁻¹ i ↔ cs.IsRightDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>hw : w ≠ 1<GOAL>∃ i, cs.IsLeftDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>hw : w ≠ 1<GOAL>∃ i, cs.IsRightDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>¬cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) = cs.length w + 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) + 1 = cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>¬cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) = cs.length w + 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i
<VAR>α : Type u_1<GOAL>Equiv.optionCongr 1 = 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<GOAL>Equiv.optionCongr (Equiv.swap x y) = Equiv.swap (some x) (some y)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>e : Equiv.Perm α<GOAL>Equiv.Perm.sign (Equiv.optionCongr e) = Equiv.Perm.sign e
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>σ : Equiv.Perm (Option α)<GOAL>(Equiv.removeNone σ).optionCongr = Equiv.swap none (σ none) * σ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>i : Option α × Equiv.Perm α<GOAL>Equiv.Perm.decomposeOption.symm i = Equiv.swap none i.1 * Equiv.optionCongr i.2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>σ : Equiv.Perm (Option α)<GOAL>Equiv.Perm.decomposeOption σ = (σ none, Equiv.removeNone σ)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>e : Equiv.Perm α<VAR>i : Option α<GOAL>(Equiv.Perm.decomposeOption.symm (none, e)) i = Option.map (⇑e) i
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>e : Equiv.Perm α<GOAL>Equiv.Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Equiv.Perm.sign e
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<GOAL>Finset.univ = Finset.map Equiv.Perm.decomposeOption.symm.toEmbedding Finset.univ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>Fintype α<VAR>m : Multiset ℕ<GOAL>(∃ g, g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>Equiv.Perm.decomposeFin.symm (p, Equiv.refl (Fin n)) = Equiv.swap 0 p
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>Equiv.Perm.decomposeFin.symm (p, 1) = Equiv.swap 0 p
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>e : Equiv.Perm (Fin n)<GOAL>(Equiv.Perm.decomposeFin.symm (p, e)) 0 = p
<VAR>n : ℕ<VAR>e : Equiv.Perm (Fin n)<VAR>p : Fin (n + 1)<VAR>x : Fin n<GOAL>(Equiv.Perm.decomposeFin.symm (p, e)) x.succ = (Equiv.swap 0 p) (e x).succ
<VAR>n : ℕ<VAR>e : Equiv.Perm (Fin (n + 1))<VAR>p : Fin (n + 2)<GOAL>(Equiv.Perm.decomposeFin.symm (p, e)) 1 = (Equiv.swap 0 p) (e 0).succ
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>e : Equiv.Perm (Fin n)<GOAL>Equiv.Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * Equiv.Perm.sign e
<VAR>n : ℕ<GOAL>Finset.univ = Finset.map Equiv.Perm.decomposeFin.symm.toEmbedding Finset.univ
<VAR>n : ℕ<GOAL>finRotate n.succ = Equiv.Perm.decomposeFin.symm (1, finRotate n)
<VAR>n : ℕ<GOAL>Equiv.Perm.sign (finRotate (n + 1)) = (-1) ^ n
<VAR>n : ℕ<GOAL>(finRotate (n + 2)).support = Finset.univ
<VAR>n : ℕ<GOAL>(finRotate (n + 2)).IsCycle
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j ≤ i<GOAL>i.cycleRange j = if j = i then 0 else j + 1
<VAR>n : ℕ<VAR>i : Fin n.succ<GOAL>i.cycleRange i = 0
<VAR>n : ℕ<VAR>i j : Fin n.succ<GOAL>i.cycleRange j = if j < i then j + 1 else if j = i then 0 else j
<VAR>n : ℕ<GOAL>Fin.cycleRange 0 = 1
<VAR>n : ℕ<GOAL>(Fin.last n).cycleRange = finRotate (n + 1)
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>⟨0, h⟩.cycleRange = 1
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Equiv.Perm.sign i.cycleRange = (-1) ^ ↑i
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i.succ.succAbove (i.cycleRange j) = (Equiv.swap 0 i.succ) j.succ
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(Equiv.symm i.cycleRange) 0 = i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>(Equiv.symm i.cycleRange) j.succ = i.succAbove j
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h0 : i ≠ 0<GOAL>i.cycleRange.IsCycle
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h0 : i ≠ 0<GOAL>i.cycleRange.cycleType = {↑i + 1}
<VAR>n : ℕ<GOAL>(Fin.cycleRange 2).IsThreeCycle
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>φ : M → N<VAR>X : Type u_5<VAR>SMul M X<VAR>Y : Type u_6<VAR>SMul N Y<VAR>self : X →ₑ[φ] Y<VAR>m : M<VAR>x : X<GOAL>self.toFun (m • x) = φ m • self.toFun x
<VAR>F : Type u_8<VAR>M : outParam (Type u_9)<VAR>N : outParam (Type u_10)<VAR>φ : outParam (M → N)<VAR>X : outParam (Type u_11)<VAR>Y : outParam (Type u_12)<VAR>SMul M X<VAR>SMul N Y<VAR>FunLike F X Y<VAR>self : MulActionSemiHomClass F φ X Y<VAR>f : F<VAR>c : M<VAR>x : X<GOAL>f (c • x) = φ c • f x
<VAR>F : Type u_8<VAR>M : Type u_9<VAR>X : Type u_10<VAR>Y : Type u_11<VAR>SMul M X<VAR>SMul M Y<VAR>FunLike F X Y<VAR>MulActionHomClass F M X Y<VAR>f : F<VAR>c : M<VAR>x : X<GOAL>f (c • x) = c • f x
<VAR>M' : Type u_1<VAR>X : Type u_5<VAR>SMul M' X<VAR>Y : Type u_6<VAR>SMul M' Y<VAR>F : Type u_8<VAR>FunLike F X Y<VAR>MulOneClass X<VAR>SMul X Y<VAR>IsScalarTower M' X Y<VAR>MulActionHomClass F X X Y<GOAL>MulActionHomClass F M' X Y
<VAR>M' : Type u_1<VAR>X : Type u_5<VAR>SMul M' X<VAR>Y : Type u_6<VAR>SMul M' Y<VAR>f : X →ₑ[id] Y<VAR>m : M'<VAR>x : X<GOAL>f (m • x) = m • f x
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>φ : M → N<VAR>X : Type u_5<VAR>SMul M X<VAR>Y : Type u_6<VAR>SMul N Y<VAR>f g : X →ₑ[φ] Y<GOAL>(∀ (x : X), f x = g x) → f = g
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>φ : M → N<VAR>X : Type u_5<VAR>SMul M X<VAR>Y : Type u_6<VAR>SMul N Y<VAR>f g : X →ₑ[φ] Y<GOAL>f = g ↔ ∀ (x : X), f x = g x