ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>W : Subspace K V₁<GOAL>(Submodule.dualPairing W).Nondegenerate
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>W : Subspace K V₁<GOAL>(Submodule.dualCopairing W).Nondegenerate
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>W W' : Subspace K V₁<GOAL>Submodule.dualAnnihilator (W ⊓ W') = Submodule.dualAnnihilator W ⊔ Submodule.dualAnnihilator W'
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>ι : Type u_1<VAR>Finite ι<VAR>W : ι → Subspace K V₁<GOAL>Submodule.dualAnnihilator (⨅ i, W i) = ⨆ i, Submodule.dualAnnihilator (W i)
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>W W' : Subspace K V₁<VAR>h : IsCompl W W'<GOAL>IsCompl (Submodule.dualAnnihilator W) (Submodule.dualAnnihilator W')
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>FiniteDimensional.finrank K ↥(LinearMap.range f.dualMap) = FiniteDimensional.finrank K ↥(LinearMap.range f)
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>Function.Injective ⇑f.dualMap ↔ Function.Surjective ⇑f
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>Module.IsReflexive K V₂<GOAL>(LinearMap.ker B).dualAnnihilator = LinearMap.range B.flip
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>FiniteDimensional K V₁<GOAL>Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>FiniteDimensional K V₂<GOAL>Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>FiniteDimensional K V₁<GOAL>Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>FiniteDimensional K V₂<GOAL>Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>FiniteDimensional K V₁<GOAL>Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>FiniteDimensional K V₂<GOAL>Function.Bijective ⇑B.flip ↔ Function.Bijective ⇑B
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K (Module.Dual K V)<VAR>FiniteDimensional K ↥W<GOAL>Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K (Module.Dual K V)<VAR>FiniteDimensional K ↥W<GOAL>Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W).flip
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K (Module.Dual K V)<VAR>FiniteDimensional K ↥W<GOAL>(Submodule.dualCoannihilator W).dualAnnihilator = W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Submodule K (Module.Dual K V)<GOAL>FiniteDimensional K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K ↥W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<VAR>FiniteDimensional K ↥W<GOAL>(Submodule.dualAnnihilator W).dualAnnihilator = Submodule.map (Module.Dual.eval K V) W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K (Module.Dual K V)<VAR>FiniteDimensional K V<GOAL>Submodule.map (Module.Dual.eval K V) (Submodule.dualCoannihilator W) = Submodule.dualAnnihilator W
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : Module.Dual R M<VAR>g : Module.Dual R N<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = f m * g n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module A M<VAR>Module R N<VAR>IsScalarTower R A M<VAR>f : Module.Dual A M<VAR>g : Module.Dual R N<VAR>m : M<VAR>n : N<GOAL>((TensorProduct.AlgebraTensorModule.dualDistrib R A M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = g n • f m
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>f : Module.Dual R (TensorProduct R M N)<GOAL>(TensorProduct.dualDistribInvOfBasis b c) f = ∑ i : ι, ∑ j : κ, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis j
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>TensorProduct.dualDistrib R M N ∘ₗ TensorProduct.dualDistribInvOfBasis b c = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>TensorProduct.dualDistribInvOfBasis b c ∘ₗ TensorProduct.dualDistrib R M N = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>a : Module.Dual R (TensorProduct R M N)<GOAL>(TensorProduct.dualDistribEquivOfBasis b c).symm a = ∑ x : ι, ∑ x_1 : κ, a (b x ⊗ₜ[R] c x_1) • b.coord x ⊗ₜ[R] c.coord x_1
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>DecidableEq ι<VAR>DecidableEq κ<VAR>Fintype ι<VAR>Fintype κ<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>∀ (a : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (a_1 : TensorProduct R M N), ((TensorProduct.dualDistribEquivOfBasis b c) a) a_1 = (TensorProduct.lid R R) (((TensorProduct.homTensorHomMap R M N R R) a) a_1)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Finite E<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Finite F<VAR>FiniteDimensional F E<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>Infinite F<VAR>E : Type u_2<VAR>Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>f g : F[X]<GOAL>∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
<VAR>F : Type u_1<VAR>Field F<VAR>Infinite F<VAR>E : Type u_2<VAR>Field E<VAR>α β : E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>Field F<VAR>Infinite F<VAR>E : Type u_2<VAR>Field E<VAR>α β : E<VAR>Algebra F E<VAR>Finite (IntermediateField F E)<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>Algebra.IsSeparable F E<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<GOAL>IsAlgebraic F α
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Finite (IntermediateField F E)<GOAL>Algebra.IsAlgebraic F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Finite (IntermediateField F E)<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Finite (IntermediateField F E)<VAR>K : IntermediateField F E<GOAL>∃ α, F⟮α⟯ = K
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>h : ∃ α, F⟮α⟯ = ⊤<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>h : ∃ α, F⟮α⟯ = ⊤<GOAL>Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>(Algebra.IsAlgebraic F E ∧ ∃ α, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>Algebra.IsSeparable F E<VAR>K : Type u_3<VAR>Field K<VAR>IsAlgClosed K<VAR>Algebra F K<GOAL>Fintype.card (E →ₐ[F] K) = FiniteDimensional.finrank F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>Algebra.IsSeparable F E<VAR>L : Type u_3<VAR>Field L<VAR>Algebra F L<VAR>hL : ∀ (x : E), Polynomial.Splits (algebraMap F L) (minpoly F x)<GOAL>Fintype.card (E →ₐ[F] L) = FiniteDimensional.finrank F E
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = FiniteDimensional.finrank F E
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(FiniteDimensional.finrank F E)
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>Field A<VAR>Algebra F A<VAR>hA : ∀ (x : E), Polynomial.Splits (algebraMap F A) (minpoly F x)<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ Function.Injective fun φ => φ α
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>Field A<VAR>Algebra F A<VAR>hA : ∀ (x : E), Polynomial.Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<GOAL>F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<VAR>x : α<GOAL>birkhoffSum f g 0 x = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<GOAL>birkhoffSum f g 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<VAR>x : α<GOAL>birkhoffSum f g 1 x = g x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<GOAL>birkhoffSum f g 1 = g
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffSum f g (n + 1) x = birkhoffSum f g n x + g (f^[n] x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffSum f g (n + 1) x = g x + birkhoffSum f g n (f x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<VAR>m n : ℕ<VAR>x : α<GOAL>birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → α<VAR>x : α<VAR>h : Function.IsFixedPt f x<VAR>g : α → M<VAR>n : ℕ<GOAL>birkhoffSum f g n x = n • g x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>F : Type u_3<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>g' : F<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>g' (birkhoffSum f g n x) = birkhoffSum f (⇑g' ∘ g) n x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>f : α → α<VAR>g : α → G<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<GOAL>f.eigenspace 0 = LinearMap.ker f
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>x : M<VAR>h : f.HasEigenvector μ x<GOAL>f.HasEigenvalue μ
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>x : M<GOAL>x ∈ f.eigenspace μ ↔ f x = μ • x
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>x : M<VAR>hx : f.HasEigenvector μ x<GOAL>f x = μ • x
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>v : M<VAR>hv : f.HasEigenvector μ v<VAR>n : ℕ<GOAL>(f ^ n) v = μ ^ n • v
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>hμ : f.HasEigenvalue μ<GOAL>∃ v, f.HasEigenvector μ v
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>h : f.HasEigenvalue μ<VAR>n : ℕ<GOAL>(f ^ n).HasEigenvalue (μ ^ n)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<VAR>hfn : IsNilpotent f<VAR>μ : R<VAR>hf : f.HasEigenvalue μ<GOAL>IsNilpotent μ
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>hμ : f.HasEigenvalue μ<GOAL>μ ∈ spectrum R f
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<GOAL>f.HasEigenvalue μ ↔ μ ∈ spectrum K f
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>a b : K<VAR>hb : b ≠ 0<GOAL>f.eigenspace (a / b) = LinearMap.ker (b • f - (algebraMap K (Module.End K V)) a)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>m : M<GOAL>m ∈ (f.genEigenspace μ) k ↔ ((f - μ • 1) ^ k) m = 0
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>k : ℕ<GOAL>(f.genEigenspace 0) k = LinearMap.ker (f ^ k)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : f.HasGenEigenvalue μ k<GOAL>k ≠ 0
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<GOAL>(f.genEigenspace μ) k ≤ f.maxGenEigenspace μ
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>m : M<GOAL>m ∈ f.maxGenEigenspace μ ↔ ∃ k, ((f - μ • 1) ^ k) m = 0
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>h : IsNoetherian R M<VAR>f : Module.End R M<VAR>μ : R<GOAL>f.maxGenEigenspace μ = (f.genEigenspace μ) (f.maxGenEigenspaceIndex μ)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k m : ℕ<VAR>hm : k ≤ m<VAR>hk : f.HasGenEigenvalue μ k<GOAL>f.HasGenEigenvalue μ m
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<GOAL>f.eigenspace μ ≤ (f.genEigenspace μ) k
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>hμ : f.HasEigenvalue μ<GOAL>f.HasGenEigenvalue μ k
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>hμ : f.HasGenEigenvalue μ k<GOAL>f.HasEigenvalue μ
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<GOAL>f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<VAR>k : ℕ<GOAL>(f.genEigenspace μ) k ≤ (f.genEigenspace μ) (FiniteDimensional.finrank K V)
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<GOAL>⨆ k, (f.genEigenspace μ) k = (f.genEigenspace μ) (FiniteDimensional.finrank K V)
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<VAR>k : ℕ<VAR>hk : FiniteDimensional.finrank K V ≤ k<GOAL>(f.genEigenspace μ) k = (f.genEigenspace μ) (FiniteDimensional.finrank K V)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f g : Module.End R M<VAR>h : Commute f g<VAR>μ : R<VAR>k : ℕ<GOAL>Set.MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f g : Module.End R M<VAR>h : Commute f g<VAR>μ : R<GOAL>Set.MapsTo ⇑g ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k) := ⋯<GOAL>IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : Module.End R M<VAR>μ : R<VAR>h : Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k) := ⋯<GOAL>IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<VAR>k l : ℕ<GOAL>Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<GOAL>Disjoint (⨆ k, (f.genEigenspace μ₁) k) (⨆ k, (f.genEigenspace μ₂) k)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<GOAL>Set.InjOn (fun x => ⨆ k, (f.genEigenspace x) k) {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<GOAL>CompleteLattice.Independent fun μ => ⨆ k, (f.genEigenspace μ) k
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<GOAL>CompleteLattice.Independent f.eigenspace
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : Module.End R M<VAR>μs : Set R<VAR>xs : ↑μs → M<VAR>h_eigenvec : ∀ (μ : ↑μs), f.HasEigenvector (↑μ) (xs μ)<GOAL>LinearIndependent (ι := ↑μs) R xs
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>p : Submodule R M<VAR>k : ℕ<VAR>μ : R<VAR>hfp : ∀ x ∈ p, f x ∈ p<GOAL>(Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k = Submodule.comap p.subtype ((f.genEigenspace μ) k)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>p : Submodule R M<VAR>k : ℕ<VAR>μ : R<VAR>hfp : ∀ x ∈ p, f x ∈ p<GOAL>p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype ((Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k)
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<GOAL>Submodule.map p.subtype (Module.End.eigenspace (LinearMap.restrict f hfp) μ) ≤ f.eigenspace μ
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>μ : K<GOAL>Disjoint (f.genEigenrange μ (FiniteDimensional.finrank K V)) ((f.genEigenspace μ) (FiniteDimensional.finrank K V))
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<VAR>hμp : Disjoint (f.eigenspace μ) p<GOAL>Module.End.eigenspace (LinearMap.restrict f hfp) μ = ⊥
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>k : ℕ<VAR>μ : K<VAR>hx : f.HasEigenvalue μ<VAR>hk : 0 < k<GOAL>0 < FiniteDimensional.finrank K ↥((f.genEigenspace μ) k)
<VAR>K : Type v<VAR>V : Type w<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>μ : K<VAR>n : ℕ<GOAL>Submodule.map f (f.genEigenrange μ n) ≤ f.genEigenrange μ n
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>μ t : R<GOAL>⨆ k, (f.genEigenspace μ) k ≤ ⨆ k, ((t • f).genEigenspace (t * μ)) k
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f₁ f₂ : Module.End R M<VAR>μ₁ μ₂ : R<VAR>h : Commute f₁ f₂<GOAL>(⨆ k, (f₁.genEigenspace μ₁) k) ⊓ ⨆ k, (f₂.genEigenspace μ₂) k ≤ ⨆ k, ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) k
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>SMul R L<VAR>FunLike F L (Module.End R M)<VAR>MulActionHomClass F R L (Module.End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>t : R<VAR>x : L<GOAL>μ (t • x) = t • μ x
<VAR>R : Type v<VAR>M : Type w<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>Add L<VAR>FunLike F L (Module.End R M)<VAR>AddHomClass F L (Module.End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<GOAL>μ (x + y) = μ x + μ y
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : α → α<VAR>g : α → M<VAR>x : α<GOAL>birkhoffAverage R f g 0 x = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : α → α<VAR>g : α → M<GOAL>birkhoffAverage R f g 0 = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : α → α<VAR>g : α → M<VAR>x : α<GOAL>birkhoffAverage R f g 1 x = g x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : α → α<VAR>g : α → M<GOAL>birkhoffAverage R f g 1 = g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>F : Type u_5<VAR>N : Type u_6<VAR>DivisionSemiring S<VAR>AddCommMonoid N<VAR>Module S N<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>g' : F<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>g' (birkhoffAverage R f g n x) = birkhoffAverage S f (⇑g' ∘ g) n x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>DivisionSemiring S<VAR>Module S M<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffAverage R f g n x = birkhoffAverage S f g n x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_4<VAR>DivisionSemiring S<VAR>Module S M<GOAL>birkhoffAverage R = birkhoffAverage S