ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>h : f = g<VAR>x : X<GOAL>f x = g 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>φ' : M → N<VAR>h : φ = φ'<VAR>f : X →ₑ[φ] Y<GOAL>(MulActionHom.ofEq h f).toFun = f.toFun
<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>φ' : M → N<VAR>h : φ = φ'<VAR>f : X →ₑ[φ] Y<VAR>a : X<GOAL>(MulActionHom.ofEq h f) a = f a
<VAR>M : Type u_2<VAR>X : Type u_5<VAR>SMul M X<VAR>x : X<GOAL>(MulActionHom.id M) x = x
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>SMul M X<VAR>Y : Type u_6<VAR>SMul N Y<VAR>Z : Type u_7<VAR>SMul P Z<VAR>g : Y →ₑ[ψ] Z<VAR>f : X →ₑ[φ] Y<VAR>CompTriple φ ψ χ<VAR>x : X<GOAL>(g.comp f) x = g (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 : X →ₑ[φ] Y<GOAL>(MulActionHom.id N).comp f = f
<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 : X →ₑ[φ] Y<GOAL>f.comp (MulActionHom.id M) = f
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>SMul M X<VAR>Y : Type u_6<VAR>SMul N Y<VAR>Z : Type u_7<VAR>SMul P Z<VAR>Q : Type u_8<VAR>T : Type u_9<VAR>SMul Q T<VAR>η : P → Q<VAR>θ : M → Q<VAR>ζ : N → Q<VAR>h : Z →ₑ[η] T<VAR>g : Y →ₑ[ψ] Z<VAR>f : X →ₑ[φ] Y<VAR>CompTriple φ ψ χ<VAR>CompTriple χ η θ<VAR>CompTriple ψ η ζ<VAR>CompTriple φ ζ θ<GOAL>h.comp (g.comp f) = (h.comp g).comp f
<VAR>M : Type u_2<VAR>X : Type u_5<VAR>SMul M X<VAR>Y₁ : Type u_8<VAR>SMul M Y₁<VAR>f : X →ₑ[id] Y₁<VAR>g : Y₁ → X<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : Y₁), (f.inverse g h₁ h₂) a = g a
<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>φ' : N → M<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : Y), (f.inverse' g k h₁ h₂) a = g a
<VAR>M : Type u_2<VAR>X : Type u_5<VAR>SMul M X<VAR>Y₁ : Type u_8<VAR>SMul M Y₁<VAR>f : X →ₑ[id] Y₁<VAR>g : Y₁ → X<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂
<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>φ' : N → M<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₁ : Function.LeftInverse φ' φ<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>(f.inverse' g k₂ h₁ h₂).inverse' (⇑f) k₁ h₂ h₁ = f
<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>φ' : N → M<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₁ : Function.LeftInverse φ' φ<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>(f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M
<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>φ' : N → M<VAR>f : X →ₑ[φ] Y<VAR>g : Y → X<VAR>k₂ : Function.RightInverse φ' φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>f.comp (f.inverse' g k₂ h₁ h₂) = MulActionHom.id N
<VAR>M : Type u_11<VAR>N : Type u_9<VAR>α : Type u_10<VAR>SMul M α<VAR>SMul N α<VAR>SMulCommClass M N α<VAR>c : M<GOAL>∀ (x : α), (SMulCommClass.toMulActionHom N α c) x = c • x
<VAR>M : Type u_13<VAR>N : Type u_11<VAR>A : Type u_12<VAR>Monoid N<VAR>AddMonoid A<VAR>DistribSMul M A<VAR>DistribMulAction N A<VAR>SMulCommClass M N A<VAR>c : M<GOAL>∀ (x : A), (SMulCommClass.toDistribMulActionHom N A c) x = c • x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<GOAL>f.toFun = ⇑f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f g : A →ₑ+[φ] B<GOAL>(∀ (x : A), f x = g x) → f = g
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f g : A →ₑ+[φ] B<GOAL>f = g ↔ ∀ (x : A), f x = g x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f g : A →ₑ+[φ] B<VAR>h : f = g<VAR>x : A<GOAL>f x = g x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f g : A →ₑ+[φ] B<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<GOAL>f 0 = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<VAR>x y : A<GOAL>f (x + y) = f x + f y
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A' : Type u_8<VAR>AddGroup A'<VAR>DistribMulAction M A'<VAR>B' : Type u_9<VAR>AddGroup B'<VAR>DistribMulAction N B'<VAR>f : A' →ₑ+[φ] B'<VAR>x : A'<GOAL>f (-x) = -f x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A' : Type u_8<VAR>AddGroup A'<VAR>DistribMulAction M A'<VAR>B' : Type u_9<VAR>AddGroup B'<VAR>DistribMulAction N B'<VAR>f : A' →ₑ+[φ] B'<VAR>x y : A'<GOAL>f (x - y) = f x - f y
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<VAR>m : M<VAR>x : A<GOAL>f (m • x) = φ m • f x
<VAR>M : Type u_1<VAR>Monoid M<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>x : A<GOAL>(DistribMulActionHom.id M) x = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<GOAL>⇑0 = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<GOAL>⇑1 = id
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>a : A<GOAL>0 a = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>a : A<GOAL>1 a = a
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>P : Type u_3<VAR>Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>C : Type u_7<VAR>AddMonoid C<VAR>DistribMulAction P C<VAR>g : B →ₑ+[ψ] C<VAR>f : A →ₑ+[φ] B<VAR>φ.CompTriple ψ χ<VAR>x : A<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<GOAL>(DistribMulActionHom.id N).comp f = f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>f : A →ₑ+[φ] B<GOAL>f.comp (DistribMulActionHom.id M) = f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>P : Type u_3<VAR>Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B : Type u_5<VAR>AddMonoid B<VAR>DistribMulAction N B<VAR>C : Type u_7<VAR>AddMonoid C<VAR>DistribMulAction P C<VAR>Q : Type u_11<VAR>D : Type u_12<VAR>Monoid Q<VAR>AddMonoid D<VAR>DistribMulAction Q D<VAR>η : P →* Q<VAR>θ : M →* Q<VAR>ζ : N →* Q<VAR>h : C →ₑ+[η] D<VAR>g : B →ₑ+[ψ] C<VAR>f : A →ₑ+[φ] B<VAR>φ.CompTriple ψ χ<VAR>χ.CompTriple η θ<VAR>ψ.CompTriple η ζ<VAR>φ.CompTriple ζ θ<GOAL>h.comp (g.comp f) = (h.comp g).comp f
<VAR>M : Type u_1<VAR>Monoid M<VAR>A : Type u_4<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>B₁ : Type u_6<VAR>AddMonoid B₁<VAR>DistribMulAction M B₁<VAR>f : A →+[M] B₁<VAR>g : B₁ → A<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : B₁), (f.inverse g h₁ h₂) a = g a
<VAR>R : Type u_11<VAR>Semiring R<VAR>S : Type u_13<VAR>Semiring S<VAR>N' : Type u_16<VAR>AddMonoid N'<VAR>DistribMulAction S N'<VAR>σ : R →* S<VAR>f g : R →ₑ+[σ] N'<VAR>h : f 1 = g 1<GOAL>f = g
<VAR>R : Type u_11<VAR>Semiring R<VAR>S : Type u_13<VAR>Semiring S<VAR>N' : Type u_16<VAR>AddMonoid N'<VAR>DistribMulAction S N'<VAR>σ : R →* S<VAR>f g : R →ₑ+[σ] N'<GOAL>f = g ↔ f 1 = g 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<GOAL>⇑↑f = ⇑f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f g : R →ₑ+*[φ] S<GOAL>(∀ (x : R), f x = g x) → f = g
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f g : R →ₑ+*[φ] S<GOAL>f = g ↔ ∀ (x : R), f x = g x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<GOAL>f 0 = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<VAR>x y : R<GOAL>f (x + y) = f x + f y
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R' : Type u_11<VAR>Ring R'<VAR>MulSemiringAction M R'<VAR>S' : Type u_13<VAR>Ring S'<VAR>MulSemiringAction N S'<VAR>f : R' →ₑ+*[φ] S'<VAR>x : R'<GOAL>f (-x) = -f x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R' : Type u_11<VAR>Ring R'<VAR>MulSemiringAction M R'<VAR>S' : Type u_13<VAR>Ring S'<VAR>MulSemiringAction N S'<VAR>f : R' →ₑ+*[φ] S'<VAR>x y : R'<GOAL>f (x - y) = f x - f y
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<GOAL>f 1 = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<VAR>x y : R<GOAL>f (x * y) = f x * f y
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<VAR>m : M<VAR>x : R<GOAL>f (m • x) = φ m • f x
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction M S<VAR>f : R →+*[M] S<VAR>m : M<VAR>x : R<GOAL>f (m • x) = m • f x
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>x : R<GOAL>(MulSemiringActionHom.id M) x = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>P : Type u_3<VAR>Monoid P<VAR>φ : M →* N<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>T : Type u_14<VAR>Semiring T<VAR>MulSemiringAction P T<VAR>g : S →ₑ+*[ψ] T<VAR>f : R →ₑ+*[φ] S<VAR>φ.CompTriple ψ χ<VAR>x : R<GOAL>(g.comp f) x = g (f x)
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<GOAL>(MulSemiringActionHom.id N).comp f = f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<GOAL>f.comp (MulSemiringActionHom.id M) = f
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_2<VAR>Monoid N<VAR>φ : M →* N<VAR>φ' : N →* M<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S : Type u_12<VAR>Semiring S<VAR>MulSemiringAction N S<VAR>f : R →ₑ+*[φ] S<VAR>g : S → R<VAR>k : Function.RightInverse ⇑φ' ⇑φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : S), (f.inverse' g k h₁ h₂) a = g a
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type u_10<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>S₁ : Type u_15<VAR>Semiring S₁<VAR>MulSemiringAction M S₁<VAR>f : R →+*[M] S₁<VAR>g : S₁ → R<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>∀ (a : S₁), (f.inverse g h₁ h₂) a = g a
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>n : ℕ<VAR>x : G<GOAL>Function.IsPeriodicPt (fun x_1 => x + x_1) n 0 ↔ n • x = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>n : ℕ<VAR>x : G<GOAL>Function.IsPeriodicPt (fun x_1 => x * x_1) n 1 ↔ x ^ n = 1
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>IsOfFinAddOrder (Additive.ofMul x) ↔ IsOfFinOrder x
<VAR>α : Type u_6<VAR>AddMonoid α<VAR>x : α<GOAL>IsOfFinOrder (Multiplicative.ofAdd x) ↔ IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>IsOfFinAddOrder x ↔ ∃ n, 0 < n ∧ n • x = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1
<VAR>G : Type u_6<VAR>AddGroup G<VAR>x : G<GOAL>IsOfFinAddOrder x ↔ ∃ n, n ≠ 0 ∧ n • x = 0
<VAR>G : Type u_6<VAR>Group G<VAR>x : G<GOAL>IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>h : Function.Injective fun n => x ^ n<GOAL>¬IsOfFinOrder x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>h : Function.Injective fun n => n • x<GOAL>¬IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>Monoid G<VAR>a : G<VAR>n : ℕ<GOAL>IsOfFinOrder a → IsOfFinOrder (a ^ n)
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>H : AddSubmonoid G<VAR>x : ↥H<GOAL>IsOfFinAddOrder ↑x ↔ IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>Monoid G<VAR>H : Submonoid G<VAR>x : ↥H<GOAL>IsOfFinOrder ↑x ↔ IsOfFinOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddMonoid G<VAR>AddMonoid H<VAR>f : G →+ H<VAR>x : G<VAR>h : IsOfFinAddOrder x<GOAL>IsOfFinAddOrder (f x)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Monoid G<VAR>Monoid H<VAR>f : G →* H<VAR>x : G<VAR>h : IsOfFinOrder x<GOAL>IsOfFinOrder (f x)
<VAR>η : Type u_6<VAR>Gs : η → Type u_7<VAR>(i : η) → AddMonoid (Gs i)<VAR>x : (i : η) → Gs i<VAR>h : IsOfFinAddOrder x<VAR>i : η<GOAL>IsOfFinAddOrder (x i)
<VAR>η : Type u_6<VAR>Gs : η → Type u_7<VAR>(i : η) → Monoid (Gs i)<VAR>x : (i : η) → Gs i<VAR>h : IsOfFinOrder x<VAR>i : η<GOAL>IsOfFinOrder (x i)
<VAR>G : Type u_1<VAR>AddMonoid G<GOAL>IsOfFinAddOrder 0
<VAR>G : Type u_1<VAR>Monoid G<GOAL>IsOfFinOrder 1
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>addOrderOf (Additive.ofMul x) = orderOf x
<VAR>α : Type u_6<VAR>AddMonoid α<VAR>a : α<GOAL>orderOf (Multiplicative.ofAdd a) = addOrderOf a
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>h : IsOfFinAddOrder x<GOAL>0 < addOrderOf x
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>h : IsOfFinOrder x<GOAL>0 < orderOf x
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>x ^ orderOf x = 1
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>addOrderOf x • x = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>h : ¬IsOfFinOrder x<GOAL>orderOf x = 0
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>h : ¬IsOfFinAddOrder x<GOAL>addOrderOf x = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>orderOf x = 0 ↔ ¬IsOfFinOrder x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>addOrderOf x = 0 ↔ ¬IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>addOrderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → n • x ≠ 0
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>h : 0 < n<GOAL>addOrderOf x = n ↔ n • x = 0 ∧ ∀ m < n, 0 < m → m • x ≠ 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>h : 0 < n<GOAL>orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>0 < addOrderOf x ↔ IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>0 < orderOf x ↔ IsOfFinOrder x
<VAR>G : Type u_1<VAR>β : Type u_5<VAR>Monoid G<VAR>x : G<VAR>Monoid β<VAR>y : β<VAR>hx : IsOfFinOrder x<VAR>h : orderOf y ∣ orderOf x<GOAL>IsOfFinOrder y
<VAR>G : Type u_1<VAR>β : Type u_5<VAR>AddMonoid G<VAR>x : G<VAR>AddMonoid β<VAR>y : β<VAR>hx : IsOfFinAddOrder x<VAR>h : addOrderOf y ∣ addOrderOf x<GOAL>IsOfFinAddOrder y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>h : n < addOrderOf x<GOAL>n • x ≠ 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>h : n < orderOf x<GOAL>x ^ n ≠ 1
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : n • x = 0<GOAL>addOrderOf x ≤ n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : x ^ n = 1<GOAL>orderOf x ≤ n
<VAR>G : Type u_1<VAR>Monoid G<GOAL>orderOf 1 = 1
<VAR>G : Type u_1<VAR>AddMonoid G<GOAL>addOrderOf 0 = 1
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>orderOf x = 1 ↔ x = 1
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>addOrderOf x = 1 ↔ x = 0
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<GOAL>(n % addOrderOf x) • x = n • x
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<GOAL>x ^ (n % orderOf x) = x ^ n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>h : x ^ n = 1<GOAL>orderOf x ∣ n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>h : n • x = 0<GOAL>addOrderOf x ∣ n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<GOAL>addOrderOf x ∣ n ↔ n • x = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<GOAL>orderOf x ∣ n ↔ x ^ n = 1
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<GOAL>orderOf (x ^ n) ∣ orderOf x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<GOAL>addOrderOf (n • x) ∣ addOrderOf x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<GOAL>Set.InjOn (fun x_1 => x_1 • x) (Set.Iio (addOrderOf x))
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<GOAL>Set.InjOn (fun x_1 => x ^ x_1) (Set.Iio (orderOf x))
<VAR>G : Type u_1<VAR>Monoid G<VAR>x y : G<VAR>DecidableEq G<VAR>hx : IsOfFinOrder x<GOAL>y ∈ Submonoid.powers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x y : G<VAR>DecidableEq G<VAR>hx : IsOfFinAddOrder x<GOAL>y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x))
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>DecidableEq G<VAR>hx : IsOfFinAddOrder x<GOAL>↑(AddSubmonoid.multiples x) = ↑(Finset.image (fun x_1 => x_1 • x) (Finset.range (addOrderOf x)))
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>DecidableEq G<VAR>hx : IsOfFinOrder x<GOAL>↑(Submonoid.powers x) = ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x)))
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<GOAL>x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<GOAL>n • x = 0 ↔ n ≡ 0 [MOD addOrderOf x]
<VAR>G : Type u_1<VAR>Monoid G<VAR>H : Type u_6<VAR>Monoid H<VAR>ψ : G →* H<VAR>x : G<GOAL>orderOf (ψ x) ∣ orderOf x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>H : Type u_6<VAR>AddMonoid H<VAR>ψ : G →+ H<VAR>x : G<GOAL>addOrderOf (ψ x) ∣ addOrderOf x
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>h : n.Coprime (orderOf x)<GOAL>∃ m, (x ^ n) ^ m = x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>h : n.Coprime (addOrderOf x)<GOAL>∃ m, m • n • x = x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : n • x = 0<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → (n / p) • x ≠ 0<GOAL>addOrderOf x = n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : x ^ n = 1<VAR>hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1<GOAL>orderOf x = n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>H : Type u_6<VAR>AddMonoid H<VAR>y : H<GOAL>addOrderOf x = addOrderOf y ↔ ∀ (n : ℕ), n • x = 0 ↔ n • y = 0
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>H : Type u_6<VAR>Monoid H<VAR>y : H<GOAL>orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
<VAR>G : Type u_1<VAR>Monoid G<VAR>H : Type u_6<VAR>Monoid H<VAR>f : G →* H<VAR>hf : Function.Injective ⇑f<VAR>x : G<GOAL>orderOf (f x) = orderOf x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>H : Type u_6<VAR>AddMonoid H<VAR>f : G →+ H<VAR>hf : Function.Injective ⇑f<VAR>x : G<GOAL>addOrderOf (f x) = addOrderOf x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>H : Type u_6<VAR>AddMonoid H<VAR>e : G ≃+ H<VAR>x : G<GOAL>addOrderOf (e x) = addOrderOf x
<VAR>G : Type u_1<VAR>Monoid G<VAR>H : Type u_6<VAR>Monoid H<VAR>e : G ≃* H<VAR>x : G<GOAL>orderOf (e x) = orderOf x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddMonoid G<VAR>x : G<VAR>AddMonoid H<VAR>f : G →+ H<VAR>hf : Function.Injective ⇑f<GOAL>IsOfFinAddOrder (f x) ↔ IsOfFinAddOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Monoid G<VAR>x : G<VAR>Monoid H<VAR>f : G →* H<VAR>hf : Function.Injective ⇑f<GOAL>IsOfFinOrder (f x) ↔ IsOfFinOrder x
<VAR>G : Type u_1<VAR>Monoid G<VAR>H : Submonoid G<VAR>y : ↥H<GOAL>orderOf ↑y = orderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>H : AddSubmonoid G<VAR>y : ↥H<GOAL>addOrderOf ↑y = addOrderOf y
<VAR>G : Type u_1<VAR>Monoid G<VAR>y : Gˣ<GOAL>orderOf ↑y = orderOf y
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>y : AddUnits G<GOAL>addOrderOf ↑y = addOrderOf y
<VAR>M : Type u_6<VAR>Monoid M<VAR>x : M<VAR>hx : IsOfFinOrder x<GOAL>↑hx.unit = x
<VAR>M : Type u_6<VAR>Monoid M<VAR>x : M<VAR>hx : IsOfFinOrder x<GOAL>↑hx.unit⁻¹ = x ^ (orderOf x - 1)
<VAR>M : Type u_6<VAR>Monoid M<VAR>x : M<VAR>hx : IsOfFinOrder x<GOAL>IsUnit x
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>dvd : n ∣ addOrderOf x<GOAL>addOrderOf (n • x) = addOrderOf x / n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>dvd : n ∣ orderOf x<GOAL>orderOf (x ^ n) = orderOf x / n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>hx : orderOf x ≠ 0<VAR>hn : n ∣ orderOf x<GOAL>orderOf (x ^ (orderOf x / n)) = n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>hx : addOrderOf x ≠ 0<VAR>hn : n ∣ addOrderOf x<GOAL>addOrderOf ((addOrderOf x / n) • x) = n
<VAR>G : Type u_1<VAR>Monoid G<VAR>x : G<VAR>n : ℕ<VAR>h : IsOfFinOrder x<GOAL>orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>x : G<VAR>n : ℕ<VAR>h : IsOfFinAddOrder x<GOAL>addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>y : G<VAR>m : ℕ<VAR>h : (addOrderOf y).Coprime m<GOAL>addOrderOf (m • y) = addOrderOf y
<VAR>G : Type u_1<VAR>Monoid G<VAR>y : G<VAR>m : ℕ<VAR>h : (orderOf y).Coprime m<GOAL>orderOf (y ^ m) = orderOf y
<VAR>G : Type u_1<VAR>Monoid G<VAR>a : G<VAR>ha : IsOfFinOrder a<GOAL>Nat.card ↑↑(Submonoid.powers a) ≤ orderOf a
<VAR>G : Type u_1<VAR>AddMonoid G<VAR>a : G<VAR>ha : IsOfFinAddOrder a<GOAL>Nat.card ↑↑(AddSubmonoid.multiples a) ≤ addOrderOf a