ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>↑f.range ⊆ ↑f.idealRange
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<GOAL>LieIdeal.map f I ≤ f.idealRange
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>J : LieIdeal R L'<GOAL>f.ker ≤ LieIdeal.comap f J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>↑f.ker = LinearMap.ker ↑f
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>x : L<GOAL>x ∈ f.ker ↔ f x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>x : L<GOAL>f x ∈ f.idealRange
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h : f.IsIdealMorphism<VAR>y : L'<GOAL>y ∈ f.idealRange ↔ ∃ x, f x = y
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<GOAL>I ≤ f.ker ↔ ∀ x ∈ I, f x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.ker = ⊥ ↔ Function.Injective ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.range.toSubmodule = LinearMap.range ↑f
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h : Function.Surjective ⇑f<GOAL>f.idealRange = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h : Function.Surjective ⇑f<GOAL>f.IsIdealMorphism
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<GOAL>LieIdeal.map f I = ⊥ ↔ I ≤ f.ker
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>h : Function.Surjective ⇑f<GOAL>↑(LieIdeal.map f I) = Submodule.map ↑f ↑I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>y : L'<VAR>h₁ : Function.Surjective ⇑f<VAR>h₂ : y ∈ LieIdeal.map f I<GOAL>∃ x, f ↑x = y
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>h₁ : Function.Injective ⇑f<VAR>h₂ : LieIdeal.map f I = ⊥<GOAL>I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I₁ I₂ : LieIdeal R L<VAR>h : I₁ ≤ I₂<VAR>x : ↥I₁<GOAL>↑((LieIdeal.inclusion h) x) = ↑x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I₁ I₂ : LieIdeal R L<VAR>h : I₁ ≤ I₂<VAR>x : ↥I₁<GOAL>(LieIdeal.inclusion h) x = ⟨↑x, ⋯⟩
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I₁ I₂ : LieIdeal R L<VAR>h : I₁ ≤ I₂<GOAL>Function.Injective ⇑(LieIdeal.inclusion h)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<GOAL>LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<GOAL>LieIdeal.map f I ⊔ LieIdeal.map f f.ker = LieIdeal.map f I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>J : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>LieIdeal.map f (LieIdeal.comap f J) = f.idealRange ⊓ J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>h : ↑(LieIdeal.map f I) = ⇑f '' ↑I<GOAL>LieIdeal.comap f (LieIdeal.map f I) = I ⊔ f.ker
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>I.incl.range = lieIdealSubalgebra R L I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<VAR>x : ↥I<GOAL>I.incl x = ↑x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>↑I.incl = (lieIdealSubalgebra R L I).subtype
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>Function.Injective ⇑I.incl
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>LieIdeal.comap I.incl I = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>I.incl.ker = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>I.incl.idealRange = I
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>I : LieIdeal R L<GOAL>I.incl.IsIdealMorphism
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>↑f.ker = LinearMap.ker ↑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>f.ker = ⊥ ↔ Function.Injective ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>m : M<GOAL>m ∈ f.ker ↔ f m = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>LieModuleHom.id.ker = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>f.comp f.ker.incl = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>M' : LieSubmodule R L M<GOAL>M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>↑f.range = Set.range ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>↑f.range = LinearMap.range ↑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>n : N<GOAL>n ∈ f.range ↔ ∃ m, f m = n
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>LieSubmodule.map f ⊤ = f.range
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup N<VAR>Module R N<VAR>LieRingModule L N<VAR>P : LieSubmodule R L N<VAR>f : M →ₗ⁅R,L⁆ N<VAR>h : ∀ (m : M), f m ∈ P<VAR>m : M<GOAL>↑((LieModuleHom.codRestrict P f h) m) = f m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>N.incl.ker = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>N.incl.range = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.comap N.incl N = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.map N.incl ⊤ = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<VAR>M' : Type u_1<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<GOAL>LieSubmodule.map f N ≤ f.range
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<VAR>N' : LieSubmodule R L ↥↑N<GOAL>LieSubmodule.map N.incl N' < N ↔ N' < ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<VAR>N' : LieSubmodule R L ↥↑N<GOAL>LieSubmodule.map N.incl N' ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : ↥⊤<GOAL>LieSubalgebra.topEquiv x = ↑x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : ↥⊤<GOAL>LieIdeal.topEquiv x = ↑x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>x : ↥⊤<GOAL>(LieModuleEquiv.ofTop R L M) x = ↑x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>M' : Type u_2<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>e : M ≃ₗ⁅R,L⁆ M'<GOAL>e.range = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>h : Function.Periodic f c<GOAL>(fun x => f (x + c)) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>h : Function.Periodic f c<VAR>g : β → γ<GOAL>Function.Periodic (g ∘ f) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>Add γ<VAR>h : Function.Periodic f c<VAR>g : AddHom γ α<VAR>g_inv : α → γ<VAR>hg : Function.RightInverse g_inv ⇑g<GOAL>Function.Periodic (f ∘ ⇑g) (g_inv c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>c : α<VAR>Add α<VAR>Add β<VAR>hf : Function.Periodic f c<VAR>hg : Function.Periodic g c<GOAL>Function.Periodic (f + g) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>c : α<VAR>Add α<VAR>Mul β<VAR>hf : Function.Periodic f c<VAR>hg : Function.Periodic g c<GOAL>Function.Periodic (f * g) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>c : α<VAR>Add α<VAR>Sub β<VAR>hf : Function.Periodic f c<VAR>hg : Function.Periodic g c<GOAL>Function.Periodic (f - g) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α → β<VAR>c : α<VAR>Add α<VAR>Div β<VAR>hf : Function.Periodic f c<VAR>hg : Function.Periodic g c<GOAL>Function.Periodic (f / g) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : α<VAR>Add α<VAR>Monoid β<VAR>l : List (α → β)<VAR>hl : ∀ f ∈ l, Function.Periodic f c<GOAL>Function.Periodic l.prod c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : α<VAR>Add α<VAR>AddMonoid β<VAR>l : List (α → β)<VAR>hl : ∀ f ∈ l, Function.Periodic f c<GOAL>Function.Periodic l.sum c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : α<VAR>Add α<VAR>AddCommMonoid β<VAR>s : Multiset (α → β)<VAR>hs : ∀ f ∈ s, Function.Periodic f c<GOAL>Function.Periodic s.sum c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : α<VAR>Add α<VAR>CommMonoid β<VAR>s : Multiset (α → β)<VAR>hs : ∀ f ∈ s, Function.Periodic f c<GOAL>Function.Periodic s.prod c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : α<VAR>Add α<VAR>AddCommMonoid β<VAR>ι : Type u_4<VAR>f : ι → α → β<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, Function.Periodic (f i) c<GOAL>Function.Periodic (∑ i ∈ s, f i) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : α<VAR>Add α<VAR>CommMonoid β<VAR>ι : Type u_4<VAR>f : ι → α → β<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, Function.Periodic (f i) c<GOAL>Function.Periodic (∏ i ∈ s, f i) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>SMul γ β<VAR>h : Function.Periodic f c<VAR>a : γ<GOAL>Function.Periodic (a • f) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>VAdd γ β<VAR>h : Function.Periodic f c<VAR>a : γ<GOAL>Function.Periodic (a +ᵥ f) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>Group γ<VAR>DistribMulAction γ α<VAR>h : Function.Periodic f c<VAR>a : γ<GOAL>Function.Periodic (fun x => f (a • x)) (a⁻¹ • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddCommMonoid α<VAR>DivisionSemiring γ<VAR>Module γ α<VAR>h : Function.Periodic f c<VAR>a : γ<GOAL>Function.Periodic (fun x => f (a • x)) (a⁻¹ • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (a * x)) (a⁻¹ * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>Group γ<VAR>DistribMulAction γ α<VAR>h : Function.Periodic f c<VAR>a : γ<GOAL>Function.Periodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>c : α<VAR>AddCommMonoid α<VAR>DivisionSemiring γ<VAR>Module γ α<VAR>h : Function.Periodic f c<VAR>a : γ<GOAL>Function.Periodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (a⁻¹ * x)) (a * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (x * a)) (c * a⁻¹)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (x * a)) (c / a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (x * a⁻¹)) (c * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>DivisionSemiring α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (x / a)) (c * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddSemigroup α<VAR>h1 : Function.Periodic f c₁<VAR>h2 : Function.Periodic f c₂<GOAL>Function.Periodic f (c₁ + c₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>x : α<GOAL>f (x - c) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddCommGroup α<VAR>h : Function.Periodic f c<GOAL>f (c - x) = f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<GOAL>Function.Periodic f (-c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c₁ c₂ : α<VAR>AddGroup α<VAR>h1 : Function.Periodic f c₁<VAR>h2 : Function.Periodic f c₂<GOAL>Function.Periodic f (c₁ - c₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddSemigroup α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (a + x)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommSemigroup α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (x + a)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommGroup α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (a - x)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommGroup α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>Function.Periodic (fun x => f (x - a)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>Function.Periodic f (n • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Semiring α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>Function.Periodic f (↑n * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>Function.Periodic f (-(n • c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>Function.Periodic f (-(↑n * c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>f (x - n • c) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>f (x - ↑n * c) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddCommGroup α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>f (n • c - x) = f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>f (↑n * c - x) = f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>Function.Periodic f (n • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>Function.Periodic f (↑n * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>f (x - n • c) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>f (x - ↑n * c) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>AddCommGroup α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>f (n • c - x) = f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c x : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>f (↑n * c - x) = f (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddZeroClass α<VAR>h : Function.Periodic f c<GOAL>f c = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<GOAL>f (-c) = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>f (n • c) = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Semiring α<VAR>h : Function.Periodic f c<VAR>n : ℕ<GOAL>f (↑n * c) = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>f (n • c) = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Ring α<VAR>h : Function.Periodic f c<VAR>n : ℤ<GOAL>f (↑n * c) = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>h : Function.Periodic f c<VAR>hc : 0 < c<VAR>x : α<GOAL>∃ y ∈ Set.Ico 0 c, f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>h : Function.Periodic f c<VAR>hc : 0 < c<VAR>x a : α<GOAL>∃ y ∈ Set.Ico a (a + c), f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>h : Function.Periodic f c<VAR>hc : 0 < c<VAR>x a : α<GOAL>∃ y ∈ Set.Ioc a (a + c), f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>h : Function.Periodic f c<VAR>hc : 0 < c<VAR>a : α<GOAL>f '' Set.Ioc a (a + c) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>h : Function.Periodic f c<VAR>hc : 0 < c<VAR>a : α<GOAL>f '' Set.Icc a (a + c) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>LinearOrderedAddCommGroup α<VAR>Archimedean α<VAR>h : Function.Periodic f c<VAR>hc : c ≠ 0<VAR>a : α<GOAL>f '' Set.uIcc a (a + c) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddZeroClass α<VAR>f : α → β<GOAL>Function.Periodic f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommGroup α<VAR>hf : Function.Periodic f c<VAR>a : ↥(AddSubgroup.zmultiples c)<VAR>x : α<GOAL>f (a +ᵥ x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddCommMonoid α<VAR>hf : Function.Periodic f c<VAR>a : ↥(AddSubmonoid.multiples c)<VAR>x : α<GOAL>f (a +ᵥ x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>h : Function.Periodic f c<VAR>a : α<GOAL>h.lift ↑a = f a
<VAR>R : Type u_4<VAR>X : Type u_5<VAR>AddZeroClass R<VAR>f : R → X<VAR>c : R<VAR>hf : Function.Periodic f c<VAR>hc : c ≠ 0<GOAL>¬Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<GOAL>(fun x => f (x + c)) = -f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Add α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<GOAL>(fun x => -f (x + c)) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<GOAL>Function.Periodic f (2 • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Semiring α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<GOAL>Function.Periodic f (2 * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddZeroClass α<VAR>Neg β<VAR>h : Function.Antiperiodic f c<GOAL>f c = -f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>Function.Periodic f ((2 * n) • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Semiring α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>Function.Periodic f (↑n * (2 * c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddMonoid α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>Function.Antiperiodic f ((2 * n + 1) • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Semiring α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℕ<GOAL>Function.Antiperiodic f (↑n * (2 * c) + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>Function.Periodic f ((2 * n) • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Ring α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>Function.Periodic f (↑n * (2 * c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>AddGroup α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>Function.Antiperiodic f ((2 * n + 1) • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>c : α<VAR>Ring α<VAR>InvolutiveNeg β<VAR>h : Function.Antiperiodic f c<VAR>n : ℤ<GOAL>Function.Antiperiodic f (↑n * (2 * c) + c)