ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Monoid β<VAR>MulAction β α<VAR>H : Subgroup α<VAR>MulAction.QuotientAction β H<VAR>b : β<VAR>q : α ⧸ H<GOAL>↑(b • Quotient.out' q) = b • q
<VAR>α : Type u<VAR>Group α<VAR>H : Subgroup α<VAR>a : α<VAR>q : α ⧸ H<GOAL>(Quotient.out' q)⁻¹ * a ^ Function.minimalPeriod (fun x => a • x) q * Quotient.out' q ∈ H
<VAR>α : Type u<VAR>Group α<VAR>H : Subgroup α<VAR>g : α<GOAL>(MulActionHom.toQuotient H) g = ↑g
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>x : β<VAR>g : α<GOAL>MulAction.ofQuotientStabilizer α x ↑g = g • x
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>x : β<VAR>g : α<GOAL>AddAction.ofQuotientStabilizer α x ↑g = g +ᵥ x
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>x : β<VAR>g : α ⧸ AddAction.stabilizer α x<GOAL>AddAction.ofQuotientStabilizer α x g ∈ AddAction.orbit α x
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>x : β<VAR>g : α ⧸ MulAction.stabilizer α x<GOAL>MulAction.ofQuotientStabilizer α x g ∈ MulAction.orbit α x
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>x : β<VAR>g : α<VAR>g' : α ⧸ AddAction.stabilizer α x<GOAL>AddAction.ofQuotientStabilizer α x (g +ᵥ g') = g +ᵥ AddAction.ofQuotientStabilizer α x g'
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>x : β<VAR>g : α<VAR>g' : α ⧸ MulAction.stabilizer α x<GOAL>MulAction.ofQuotientStabilizer α x (g • g') = g • MulAction.ofQuotientStabilizer α x g'
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>x : β<GOAL>Function.Injective (AddAction.ofQuotientStabilizer α x)
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>x : β<GOAL>Function.Injective (MulAction.ofQuotientStabilizer α x)
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>b : β<VAR>Fintype α<VAR>Fintype ↑(AddAction.orbit α b)<VAR>Fintype ↥(AddAction.stabilizer α b)<GOAL>Fintype.card ↑(AddAction.orbit α b) * Fintype.card ↥(AddAction.stabilizer α b) = Fintype.card α
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>b : β<VAR>Fintype α<VAR>Fintype ↑(MulAction.orbit α b)<VAR>Fintype ↥(MulAction.stabilizer α b)<GOAL>Fintype.card ↑(MulAction.orbit α b) * Fintype.card ↥(MulAction.stabilizer α b) = Fintype.card α
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>b : β<VAR>a : α<GOAL>↑((AddAction.orbitEquivQuotientStabilizer α b).symm ↑a) = a +ᵥ b
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>b : β<VAR>a : α<GOAL>↑((MulAction.orbitEquivQuotientStabilizer α b).symm ↑a) = a • b
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>MulAction.stabilizer G ↑1 = H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<GOAL>AddAction.stabilizer G ↑0 = H
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>Fintype α<VAR>Fintype β<VAR>Fintype (Quotient (MulAction.orbitRel α β))<VAR>(b : β) → Fintype ↥(MulAction.stabilizer α b)<VAR>φ : Quotient (MulAction.orbitRel α β) → β<VAR>hφ : Function.LeftInverse Quotient.mk'' φ<GOAL>Fintype.card β = ∑ ω : Quotient (MulAction.orbitRel α β), Fintype.card α / Fintype.card ↥(MulAction.stabilizer α (φ ω))
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>Fintype α<VAR>Fintype β<VAR>Fintype (Quotient (AddAction.orbitRel α β))<VAR>(b : β) → Fintype ↥(AddAction.stabilizer α b)<VAR>φ : Quotient (AddAction.orbitRel α β) → β<VAR>hφ : Function.LeftInverse Quotient.mk'' φ<GOAL>Fintype.card β = ∑ ω : Quotient (AddAction.orbitRel α β), Fintype.card α / Fintype.card ↥(AddAction.stabilizer α (φ ω))
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>Fintype α<VAR>Fintype β<VAR>Fintype (Quotient (MulAction.orbitRel α β))<VAR>(b : β) → Fintype ↥(MulAction.stabilizer α b)<GOAL>Fintype.card β = ∑ ω : Quotient (MulAction.orbitRel α β), Fintype.card α / Fintype.card ↥(MulAction.stabilizer α ω.out')
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>Fintype α<VAR>Fintype β<VAR>Fintype (Quotient (AddAction.orbitRel α β))<VAR>(b : β) → Fintype ↥(AddAction.stabilizer α b)<GOAL>Fintype.card β = ∑ ω : Quotient (AddAction.orbitRel α β), Fintype.card α / Fintype.card ↥(AddAction.stabilizer α ω.out')
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>MulAction α β<VAR>Fintype α<VAR>(a : α) → Fintype ↑(MulAction.fixedBy β a)<VAR>Fintype (Quotient (MulAction.orbitRel α β))<GOAL>∑ a : α, Fintype.card ↑(MulAction.fixedBy β a) = Fintype.card (Quotient (MulAction.orbitRel α β)) * Fintype.card α
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddAction α β<VAR>Fintype α<VAR>(a : α) → Fintype ↑(AddAction.fixedBy β a)<VAR>Fintype (Quotient (AddAction.orbitRel α β))<GOAL>∑ a : α, Fintype.card ↑(AddAction.fixedBy β a) = Fintype.card (Quotient (AddAction.orbitRel α β)) * Fintype.card α
<VAR>G : Type u_1<VAR>Group G<VAR>Fintype G<VAR>g : G<VAR>Fintype ↑(ConjClasses.mk g).carrier<VAR>Fintype ↥(MulAction.stabilizer (ConjAct G) g)<GOAL>Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<GOAL>H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker
<VAR>G : Type u_1<VAR>Group G<VAR>g x : G<GOAL>(Subgroup.quotientCentralizerEmbedding g) ↑x = ⟨⁅x, g⁆, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>S : Set G<VAR>hS : Subgroup.closure S = ⊤<VAR>g : G<VAR>s : ↑S<GOAL>(Subgroup.quotientCenterEmbedding hS) (↑g) s = ⟨⁅g, ↑s⁆, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<GOAL>Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G
<VAR>α : Type u<VAR>β : Type v<VAR>AddCommGroup β<VAR>f : α → β<VAR>x : α<GOAL>(FreeAbelianGroup.lift f) (FreeAbelianGroup.of x) = f x
<VAR>α : Type u<VAR>β : Type v<VAR>AddCommGroup β<VAR>f : α → β<VAR>g : FreeAbelianGroup α →+ β<VAR>hg : ∀ (x : α), g (FreeAbelianGroup.of x) = f x<VAR>x : FreeAbelianGroup α<GOAL>g x = (FreeAbelianGroup.lift f) x
<VAR>α : Type u<VAR>β : Type v<VAR>AddCommGroup β<VAR>g h : FreeAbelianGroup α →+ β<VAR>H : ∀ (x : α), g (FreeAbelianGroup.of x) = h (FreeAbelianGroup.of x)<GOAL>g = h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup β<VAR>AddCommGroup γ<VAR>a : FreeAbelianGroup α<VAR>f : α → β<VAR>g : β →+ γ<GOAL>g ((FreeAbelianGroup.lift f) a) = (FreeAbelianGroup.lift (⇑g ∘ f)) a
<VAR>α : Type u<GOAL>Function.Injective FreeAbelianGroup.of
<VAR>α : Type u<VAR>C : FreeAbelianGroup α → Prop<VAR>z : FreeAbelianGroup α<VAR>C0 : C 0<VAR>C1 : ∀ (x : α), C (FreeAbelianGroup.of x)<VAR>Cn : ∀ (x : α), C (FreeAbelianGroup.of x) → C (-FreeAbelianGroup.of x)<VAR>Cp : ∀ (x y : FreeAbelianGroup α), C x → C y → C (x + y)<GOAL>C z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f g : α → β<GOAL>(FreeAbelianGroup.lift (f + g)) a = (FreeAbelianGroup.lift f) a + (FreeAbelianGroup.lift g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup β<VAR>a : FreeAbelianGroup α<VAR>f : α → β<GOAL>(FreeAbelianGroup.liftAddGroupHom β a) f = (FreeAbelianGroup.lift f) a
<VAR>α : Type u<VAR>β : Type u_1<VAR>AddCommGroup β<VAR>f : α → β<GOAL>FreeAbelianGroup.lift (-f) = -FreeAbelianGroup.lift f
<VAR>α : Type u<VAR>C : FreeAbelianGroup α → Prop<VAR>z : FreeAbelianGroup α<VAR>C0 : C 0<VAR>C1 : ∀ (x : α), C (pure x)<VAR>Cn : ∀ (x : α), C (pure x) → C (-pure x)<VAR>Cp : ∀ (x y : FreeAbelianGroup α), C x → C y → C (x + y)<GOAL>C z
<VAR>α β : Type u<VAR>f : α → β<VAR>x : α<GOAL>f <$> pure x = pure (f x)
<VAR>α β : Type u<VAR>f : α → β<GOAL>f <$> 0 = 0
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeAbelianGroup α<GOAL>f <$> (x + y) = f <$> x + f <$> y
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeAbelianGroup α<GOAL>f <$> (-x) = -f <$> x
<VAR>α β : Type u<VAR>f : α → β<VAR>x y : FreeAbelianGroup α<GOAL>f <$> (x - y) = f <$> x - f <$> y
<VAR>α β : Type u<VAR>f : α → β<VAR>y : α<GOAL>f <$> FreeAbelianGroup.of y = FreeAbelianGroup.of (f y)
<VAR>α β : Type u<VAR>f : α → FreeAbelianGroup β<VAR>x : α<GOAL>pure x >>= f = f x
<VAR>α β : Type u<VAR>f : α → FreeAbelianGroup β<GOAL>0 >>= f = 0
<VAR>α β : Type u<VAR>f : α → FreeAbelianGroup β<VAR>x y : FreeAbelianGroup α<GOAL>x + y >>= f = (x >>= f) + (y >>= f)
<VAR>α β : Type u<VAR>f : α → FreeAbelianGroup β<VAR>x : FreeAbelianGroup α<GOAL>-x >>= f = -(x >>= f)
<VAR>α β : Type u<VAR>f : α → FreeAbelianGroup β<VAR>x y : FreeAbelianGroup α<GOAL>x - y >>= f = (x >>= f) - (y >>= f)
<VAR>α β : Type u<VAR>f : α → β<VAR>x : FreeAbelianGroup α<GOAL>(Seq.seq (pure f) fun x_1 => x) = f <$> x
<VAR>α β : Type u<VAR>x : FreeAbelianGroup α<GOAL>(Seq.seq 0 fun x_1 => x) = 0
<VAR>α β : Type u<VAR>f g : FreeAbelianGroup (α → β)<VAR>x : FreeAbelianGroup α<GOAL>(Seq.seq (f + g) fun x_1 => x) = (Seq.seq f fun x_1 => x) + Seq.seq g fun x_1 => x
<VAR>α β : Type u<VAR>f : FreeAbelianGroup (α → β)<VAR>x : FreeAbelianGroup α<GOAL>(Seq.seq (-f) fun x_1 => x) = -Seq.seq f fun x_1 => x
<VAR>α β : Type u<VAR>f g : FreeAbelianGroup (α → β)<VAR>x : FreeAbelianGroup α<GOAL>(Seq.seq (f - g) fun x_1 => x) = (Seq.seq f fun x_1 => x) - Seq.seq g fun x_1 => x
<VAR>α β : Type u<VAR>f : FreeAbelianGroup (α → β)<GOAL>(Seq.seq f fun x => 0) = 0
<VAR>α β : Type u<VAR>f : FreeAbelianGroup (α → β)<VAR>x y : FreeAbelianGroup α<GOAL>(Seq.seq f fun x_1 => x + y) = (Seq.seq f fun x_1 => x) + Seq.seq f fun x => y
<VAR>α β : Type u<VAR>f : FreeAbelianGroup (α → β)<VAR>x : FreeAbelianGroup α<GOAL>(Seq.seq f fun x_1 => -x) = -Seq.seq f fun x_1 => x
<VAR>α β : Type u<VAR>f : FreeAbelianGroup (α → β)<VAR>x y : FreeAbelianGroup α<GOAL>(Seq.seq f fun x_1 => x - y) = (Seq.seq f fun x_1 => x) - Seq.seq f fun x => y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommGroup γ<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>(FreeAbelianGroup.lift (g ∘ f)) x = (FreeAbelianGroup.lift g) ((FreeAbelianGroup.map f) x)
<VAR>α : Type u<GOAL>FreeAbelianGroup.map id = AddMonoidHom.id (FreeAbelianGroup α)
<VAR>α : Type u<VAR>x : FreeAbelianGroup α<GOAL>(FreeAbelianGroup.map id) x = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<GOAL>FreeAbelianGroup.map (g ∘ f) = (FreeAbelianGroup.map g).comp (FreeAbelianGroup.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>(FreeAbelianGroup.map (g ∘ f)) x = (FreeAbelianGroup.map g) ((FreeAbelianGroup.map f) x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>(FreeAbelianGroup.map f) (FreeAbelianGroup.of a) = FreeAbelianGroup.of (f a)
<VAR>α : Type u<VAR>Mul α<VAR>x y : FreeAbelianGroup α<GOAL>x * y = (FreeAbelianGroup.lift fun x₂ => (FreeAbelianGroup.lift fun x₁ => FreeAbelianGroup.of (x₁ * x₂)) x) y
<VAR>α : Type u<VAR>Mul α<VAR>x y : α<GOAL>FreeAbelianGroup.of x * FreeAbelianGroup.of y = FreeAbelianGroup.of (x * y)
<VAR>α : Type u<VAR>Mul α<VAR>x y : α<GOAL>FreeAbelianGroup.of (x * y) = FreeAbelianGroup.of x * FreeAbelianGroup.of y
<VAR>α : Type u<VAR>Monoid α<GOAL>⇑FreeAbelianGroup.ofMulHom = FreeAbelianGroup.of
<VAR>α : Type u<VAR>R : Type u_1<VAR>Monoid α<VAR>Ring R<VAR>f : α →* R<GOAL>↑(FreeAbelianGroup.liftMonoid f) = FreeAbelianGroup.lift ⇑f
<VAR>α : Type u<VAR>R : Type u_1<VAR>Monoid α<VAR>Ring R<VAR>f : α →* R<GOAL>⇑(FreeAbelianGroup.liftMonoid f) = ⇑(FreeAbelianGroup.lift ⇑f)
<VAR>α : Type u<VAR>R : Type u_1<VAR>Monoid α<VAR>Ring R<VAR>f : FreeAbelianGroup α →+* R<GOAL>⇑(FreeAbelianGroup.liftMonoid.symm f) = FreeAbelianGroup.lift.symm ↑f
<VAR>α : Type u<VAR>Monoid α<GOAL>1 = FreeAbelianGroup.of 1
<VAR>α : Type u<VAR>Monoid α<GOAL>FreeAbelianGroup.of 1 = 1
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a₁ a₂ : α<GOAL>a₂ ∈ AddAction.orbit M a₁ ↔ ∃ x, x +ᵥ a₁ = a₂
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a₁ a₂ : α<GOAL>a₂ ∈ MulAction.orbit M a₁ ↔ ∃ x, x • a₁ = a₂
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<VAR>m : M<GOAL>m • a ∈ MulAction.orbit M a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<VAR>m : M<GOAL>m +ᵥ a ∈ AddAction.orbit M a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<GOAL>a ∈ MulAction.orbit M a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<GOAL>a ∈ AddAction.orbit M a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<GOAL>(AddAction.orbit M a).Nonempty
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<GOAL>(MulAction.orbit M a).Nonempty
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>Set.MapsTo (fun x => m • x) (MulAction.orbit M a) (MulAction.orbit M a)
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>Set.MapsTo (fun x => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a)
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>m • MulAction.orbit M a ⊆ MulAction.orbit M a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>m +ᵥ AddAction.orbit M a ⊆ AddAction.orbit M a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>AddAction.orbit M (m +ᵥ a) ⊆ AddAction.orbit M a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>MulAction.orbit M (m • a) ⊆ MulAction.orbit M a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<VAR>m : M<VAR>a' : ↑(AddAction.orbit M a)<GOAL>↑(m +ᵥ a') = m +ᵥ ↑a'
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<VAR>m : M<VAR>a' : ↑(MulAction.orbit M a)<GOAL>↑(m • a') = m • ↑a'
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>S : AddSubmonoid M<VAR>a : α<GOAL>AddAction.orbit (↥S) a ⊆ AddAction.orbit M a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>S : Submonoid M<VAR>a : α<GOAL>MulAction.orbit (↥S) a ⊆ MulAction.orbit M a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>S : Submonoid M<VAR>a b : α<VAR>h : a ∈ MulAction.orbit (↥S) b<GOAL>a ∈ MulAction.orbit M b
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>S : AddSubmonoid M<VAR>a b : α<VAR>h : a ∈ AddAction.orbit (↥S) b<GOAL>a ∈ AddAction.orbit M b
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>β : Type u_1<VAR>MulAction M β<VAR>x y : α × β<VAR>h : x ∈ MulAction.orbit M y<GOAL>x.1 ∈ MulAction.orbit M y.1
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>β : Type u_1<VAR>AddAction M β<VAR>x y : α × β<VAR>h : x ∈ AddAction.orbit M y<GOAL>x.1 ∈ AddAction.orbit M y.1
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>β : Type u_1<VAR>AddAction M β<VAR>x y : α × β<VAR>h : x ∈ AddAction.orbit M y<GOAL>x.2 ∈ AddAction.orbit M y.2
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>β : Type u_1<VAR>MulAction M β<VAR>x y : α × β<VAR>h : x ∈ MulAction.orbit M y<GOAL>x.2 ∈ MulAction.orbit M y.2
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>AddAction.IsPretransitive M α<VAR>a : α<GOAL>AddAction.orbit M a = Set.univ
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>MulAction.IsPretransitive M α<VAR>a : α<GOAL>MulAction.orbit M a = Set.univ
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<GOAL>MulAction.fixedPoints M α = ⋂ m, MulAction.fixedBy α m
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<GOAL>AddAction.fixedPoints M α = ⋂ m, AddAction.fixedBy α m
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<GOAL>a ∈ MulAction.fixedPoints M α ↔ ∀ (m : M), m • a = a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<GOAL>a ∈ AddAction.fixedPoints M α ↔ ∀ (m : M), m +ᵥ a = a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>m : M<VAR>a : α<GOAL>a ∈ MulAction.fixedBy α m ↔ m • a = a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>m : M<VAR>a : α<GOAL>a ∈ AddAction.fixedBy α m ↔ m +ᵥ a = a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<GOAL>a ∈ AddAction.fixedPoints M α ↔ ∀ a' ∈ AddAction.orbit M a, a' = a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<GOAL>a ∈ MulAction.fixedPoints M α ↔ ∀ a' ∈ MulAction.orbit M a, a' = a
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<VAR>Fintype ↑(MulAction.orbit M a)<GOAL>a ∈ MulAction.fixedPoints M α ↔ Fintype.card ↑(MulAction.orbit M a) = 1
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<VAR>Fintype ↑(AddAction.orbit M a)<GOAL>a ∈ AddAction.fixedPoints M α ↔ Fintype.card ↑(AddAction.orbit M a) = 1
<VAR>M : Type u<VAR>Monoid M<VAR>α : Type v<VAR>MulAction M α<VAR>a : α<VAR>m : M<GOAL>m ∈ MulAction.stabilizerSubmonoid M a ↔ m • a = a
<VAR>M : Type u<VAR>AddMonoid M<VAR>α : Type v<VAR>AddAction M α<VAR>a : α<VAR>m : M<GOAL>m ∈ AddAction.stabilizerAddSubmonoid M a ↔ m +ᵥ a = a
<VAR>M : Type u<VAR>α : Type v<VAR>Monoid M<VAR>Monoid α<VAR>MulDistribMulAction M α<VAR>a : α<GOAL>a ∈ FixedPoints.submonoid M α ↔ ∀ (m : M), m • a = a
<VAR>M : Type u<VAR>α : Type v<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction M α<VAR>a : α<GOAL>a ∈ FixedPoints.subgroup M α ↔ ∀ (m : M), m • a = a
<VAR>M : Type u<VAR>α : Type v<VAR>Monoid M<VAR>Group α<VAR>MulDistribMulAction M α<GOAL>(FixedPoints.subgroup M α).toSubmonoid = FixedPoints.submonoid M α
<VAR>M : Type u<VAR>α : Type v<VAR>Monoid M<VAR>AddMonoid α<VAR>DistribMulAction M α<VAR>a : α<GOAL>a ∈ FixedPoints.addSubmonoid M α ↔ ∀ (m : M), m • a = a
<VAR>M : Type u<VAR>α : Type v<VAR>Monoid M<VAR>AddGroup α<VAR>DistribMulAction M α<VAR>a : α<GOAL>a ∈ α^+M ↔ ∀ (m : M), m • a = a
<VAR>M : Type u<VAR>α : Type v<VAR>Monoid M<VAR>AddGroup α<VAR>DistribMulAction M α<GOAL>(α^+M).toAddSubmonoid = FixedPoints.addSubmonoid M α
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>NonUnitalNonAssocRing R<VAR>DistribMulAction M R<VAR>k : M<VAR>h : ∀ (x : R), k • x = 0 → x = 0<VAR>a b : R<VAR>h' : k • a = k • b<GOAL>a = b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>g • MulAction.orbit G a = MulAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>g +ᵥ AddAction.orbit G a = AddAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>AddAction.orbit G (g +ᵥ a) = AddAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>MulAction.orbit G (g • a) = MulAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a b : α<GOAL>AddAction.orbit G a = AddAction.orbit G b ↔ a ∈ AddAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a b : α<GOAL>MulAction.orbit G a = MulAction.orbit G b ↔ a ∈ MulAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g : G<VAR>a : α<GOAL>a ∈ AddAction.orbit G (g +ᵥ a)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g : G<VAR>a : α<GOAL>a ∈ MulAction.orbit G (g • a)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>g h : G<VAR>a : α<GOAL>g • a ∈ MulAction.orbit G (h • a)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>g h : G<VAR>a : α<GOAL>g +ᵥ a ∈ AddAction.orbit G (h +ᵥ a)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>a : α<GOAL>AddAction.orbit (↥H) a ⊆ AddAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>a : α<GOAL>MulAction.orbit (↥H) a ⊆ MulAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>a b : α<VAR>h : a ∈ AddAction.orbit (↥H) b<GOAL>a ∈ AddAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>a b : α<VAR>h : a ∈ MulAction.orbit (↥H) b<GOAL>a ∈ MulAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a₁ a₂ : α<GOAL>a₁ ∈ MulAction.orbit G a₂ ↔ a₂ ∈ MulAction.orbit G a₁
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a₁ a₂ : α<GOAL>a₁ ∈ AddAction.orbit G a₂ ↔ a₂ ∈ AddAction.orbit G a₁
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<VAR>x : α<VAR>a b : ↑(AddAction.orbit G x)<GOAL>a ∈ AddAction.orbit (↥H) b ↔ ↑a ∈ AddAction.orbit ↥H ↑b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<VAR>x : α<VAR>a b : ↑(MulAction.orbit G x)<GOAL>a ∈ MulAction.orbit (↥H) b ↔ ↑a ∈ MulAction.orbit ↥H ↑b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a b : α<GOAL>(AddAction.orbitRel G α).Rel a b ↔ a ∈ AddAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a b : α<GOAL>(MulAction.orbitRel G α).Rel a b ↔ a ∈ MulAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a b : α<GOAL>Setoid.r a b ↔ a ∈ MulAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a b : α<GOAL>Setoid.r a b ↔ a ∈ AddAction.orbit G b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>H : Subgroup G<GOAL>MulAction.orbitRel (↥H) α ≤ MulAction.orbitRel G α
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>H : AddSubgroup G<GOAL>AddAction.orbitRel (↥H) α ≤ AddAction.orbitRel G α
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>U : Set α<GOAL>Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g +ᵥ x) '' U
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>U : Set α<GOAL>Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g • x) '' U
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>U V : Set α<GOAL>Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>U V : Set α<GOAL>Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>U V : Set α<GOAL>Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>U V : Set α<GOAL>Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>AddAction.IsPretransitive G α ↔ Subsingleton (AddAction.orbitRel.Quotient G α)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>MulAction.IsPretransitive G α ↔ Subsingleton (MulAction.orbitRel.Quotient G α)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>Nonempty α<GOAL>MulAction.IsPretransitive G α ↔ Nonempty (Unique (MulAction.orbitRel.Quotient G α))
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>Nonempty α<GOAL>AddAction.IsPretransitive G α ↔ Nonempty (Unique (AddAction.orbitRel.Quotient G α))
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a : α<GOAL>MulAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = MulAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a : α<GOAL>AddAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = AddAction.orbit G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>a : α<VAR>x : MulAction.orbitRel.Quotient G α<GOAL>a ∈ x.orbit ↔ Quotient.mk'' a = x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>a : α<VAR>x : AddAction.orbitRel.Quotient G α<GOAL>a ∈ x.orbit ↔ Quotient.mk'' a = x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<VAR>x : MulAction.orbitRel.Quotient G α<VAR>φ : MulAction.orbitRel.Quotient G α → α<VAR>hφ : Function.RightInverse φ Quotient.mk'<GOAL>x.orbit = MulAction.orbit G (φ x)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<VAR>x : AddAction.orbitRel.Quotient G α<VAR>φ : AddAction.orbitRel.Quotient G α → α<VAR>hφ : Function.RightInverse φ Quotient.mk'<GOAL>x.orbit = AddAction.orbit G (φ x)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>AddGroup G<VAR>AddAction G α<GOAL>Function.Injective AddAction.orbitRel.Quotient.orbit
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>Group G<VAR>MulAction G α<GOAL>Function.Injective MulAction.orbitRel.Quotient.orbit