ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>CommRing K<VAR>IsDomain K<VAR>p q : K[X]<GOAL>RatFunc.mk p q = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p q : K[X]<GOAL>RatFunc.mk p q = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : K[X]<GOAL>RatFunc.mk p 0 = { toFractionRing := 0 }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : K[X]<VAR>q : ↥K[X]⁰<GOAL>RatFunc.mk p ↑q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p q }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ∈ K[X]⁰<GOAL>RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, hq⟩ }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, ⋯⟩ }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : K[X]<GOAL>RatFunc.mk p 1 = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p q p' q' : K[X]<VAR>hq : q ≠ 0<VAR>hq' : q' ≠ 0<GOAL>RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q' := ⋯<GOAL>(RatFunc.mk p q).liftOn f H = f p q
<VAR>K : Type u_1<VAR>CommRing K<VAR>IsDomain K<VAR>P : Sort u_2<VAR>x : RatFunc K<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<GOAL>x.liftOn' f H = x.liftOn f ⋯
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<GOAL>(RatFunc.mk p q).liftOn' f H = f p q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>P : RatFunc K → Prop<VAR>x : RatFunc K<VAR>_pq : ∀ (p q : K[X]), q ≠ 0 → P (RatFunc.mk p q)<GOAL>P x
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<VAR>DecidableEq σ<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < (Fintype.card K - 1) * Fintype.card σ<GOAL>∑ x : σ → K, (MvPolynomial.eval x) f = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<VAR>DecidableEq σ<VAR>DecidableEq K<VAR>p : ℕ<VAR>CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<VAR>DecidableEq σ<VAR>DecidableEq K<VAR>p : ℕ<VAR>CharP K p<VAR>Fintype ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i : ι, (f i).totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // ∀ (i : ι), (MvPolynomial.eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<VAR>DecidableEq σ<VAR>DecidableEq K<VAR>p : ℕ<VAR>CharP K p<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // (MvPolynomial.eval x) f = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>Fintype K<VAR>Field K<VAR>Fintype σ<VAR>DecidableEq σ<VAR>DecidableEq K<VAR>p : ℕ<VAR>CharP K p<VAR>f₁ f₂ : MvPolynomial σ K<VAR>h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // (MvPolynomial.eval x) f₁ = 0 ∧ (MvPolynomial.eval x) f₂ = 0 }
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>self : PerfectRing R p<GOAL>Function.Bijective ⇑(frobenius R p)
<VAR>R : Type u_2<VAR>p : ℕ<VAR>CommRing R<VAR>ExpChar R p<VAR>IsReduced R<VAR>h : Function.Surjective ⇑(frobenius R p)<GOAL>PerfectRing R p
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>Function.Bijective ⇑(frobenius R p)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>Function.Bijective ⇑(iterateFrobenius R p n)
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>Function.Injective ⇑(frobenius R p)
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>Function.Surjective ⇑(frobenius R p)
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>a : R<GOAL>(frobeniusEquiv R p) a = (frobenius R p) a
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>⇑(frobeniusEquiv R p) = ⇑(frobenius R p)
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(frobeniusEquiv R p) x = x ^ p
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>a : R<GOAL>(iterateFrobeniusEquiv R p n) a = (iterateFrobenius R p n) a
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>⇑(iterateFrobeniusEquiv R p n) = ⇑(iterateFrobenius R p n)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p n) x = x ^ p ^ n
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p (m + n)) x = (iterateFrobeniusEquiv R p m) ((iterateFrobeniusEquiv R p n) x)
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>iterateFrobeniusEquiv R p (m + n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m)
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p (m + n)).symm x = (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x)
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>(iterateFrobeniusEquiv R p (m + n)).symm = (iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p 0) x = x
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p 1) x = x ^ p
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>iterateFrobeniusEquiv R p 0 = RingEquiv.refl R
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>(iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(frobeniusEquiv R p).symm ((frobenius R p) x) = x
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(frobenius R p) ((frobeniusEquiv R p).symm x) = x
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>(frobenius R p).comp ↑(frobeniusEquiv R p).symm = RingHom.id R
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>(↑(frobeniusEquiv R p).symm).comp (frobenius R p) = RingHom.id R
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x : R<GOAL>(frobeniusEquiv R p).symm x ^ p = x
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>x y : R<VAR>h : x ^ p = y ^ p<GOAL>x = y
<VAR>R : Type u_1<VAR>p : ℕ<VAR>CommSemiring R<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>f : R[X]<GOAL>(Polynomial.expand R p) f = Polynomial.map (↑(frobeniusEquiv R p).symm) f ^ p
<VAR>R : Type u_2<VAR>p : ℕ<VAR>CommSemiring R<VAR>Fact (Nat.Prime p)<VAR>CharP R p<VAR>PerfectRing R p<VAR>f : R[X]<GOAL>¬Irreducible ((Polynomial.expand R p) f)
<VAR>K : Type u_1<VAR>Field K<VAR>self : PerfectField K<VAR>f : K[X]<GOAL>Irreducible f → f.Separable
<VAR>K : Type u_1<VAR>p : ℕ<VAR>Field K<VAR>ExpChar K p<VAR>PerfectRing K p<GOAL>PerfectField K
<VAR>K : Type u_1<VAR>Field K<VAR>PerfectField K<VAR>g : K[X]<GOAL>g.Separable ↔ Squarefree g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra.IsAlgebraic K L<VAR>PerfectField K<GOAL>PerfectField L
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<GOAL>Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots ≤ p ^ n • f.roots
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<GOAL>Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots ≤ p • f.roots
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>DecidableEq R<GOAL>Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>DecidableEq R<GOAL>Finset.image (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset ⊆ f.roots.toFinset
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<GOAL>((Polynomial.expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<GOAL>((Polynomial.expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>y : R<GOAL>(Polynomial.X ^ p ^ n - Polynomial.C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>y : R<VAR>m : ℕ<GOAL>((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>y : R<GOAL>(Polynomial.X ^ p - Polynomial.C y).roots = p • {(frobeniusEquiv R p).symm y}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>PerfectRing R p<VAR>y : R<VAR>m : ℕ<GOAL>((Polynomial.X ^ p - Polynomial.C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<GOAL>Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • f.roots
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<GOAL>Multiset.map (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots = p • f.roots
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<VAR>DecidableEq R<GOAL>Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<VAR>DecidableEq R<GOAL>Finset.image (⇑(frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset = f.roots.toFinset
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>DecidableEq R<VAR>x : { x // x ∈ ((Polynomial.expand R p) f).roots.toFinset }<GOAL>↑((Polynomial.rootsExpandToRoots p f) x) = ↑x ^ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>DecidableEq R<VAR>x : { x // x ∈ ((Polynomial.expand R (p ^ n)) f).roots.toFinset }<GOAL>↑((Polynomial.rootsExpandPowToRoots p n f) x) = ↑x ^ p ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<VAR>DecidableEq R<VAR>x : { x // x ∈ ((Polynomial.expand R p) f).roots.toFinset }<GOAL>↑((Polynomial.rootsExpandEquivRoots p f) x) = ↑x ^ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>p : ℕ<VAR>ExpChar R p<VAR>f : R[X]<VAR>PerfectRing R p<VAR>DecidableEq R<VAR>n : ℕ<VAR>x : { x // x ∈ ((Polynomial.expand R (p ^ n)) f).roots.toFinset }<GOAL>↑((Polynomial.rootsExpandPowEquivRoots p f n) x) = ↑x ^ p ^ n
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<VAR>f : Module.End R M<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<GOAL>∃ μ, f.HasEigenvalue μ
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>IsAlgClosed K<VAR>FiniteDimensional K V<VAR>Nontrivial V<VAR>f : Module.End K V<GOAL>∃ c, f.HasEigenvalue c
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>IsAlgClosed K<VAR>FiniteDimensional K V<VAR>f : Module.End K V<GOAL>⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<VAR>f : Module.End K V<VAR>FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>p ⊓ ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⨆ μ, ⨆ k, p ⊓ (f.genEigenspace μ) k
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<VAR>f : Module.End K V<VAR>FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<GOAL>p = ⨆ μ, ⨆ k, p ⊓ (f.genEigenspace μ) k
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<VAR>f : Module.End K V<VAR>FiniteDimensional K V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<GOAL>⨆ μ, ⨆ k, (Module.End.genEigenspace (LinearMap.restrict f h) μ) k = ⊤
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>φ : Module.End R M<VAR>h : IsNilpotent φ<GOAL>LinearMap.charpoly φ = Polynomial.X ^ FiniteDimensional.finrank R M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>IsNoetherian R M<VAR>φ : Module.End R M<GOAL>[IsNilpotent φ, LinearMap.charpoly φ = Polynomial.X ^ FiniteDimensional.finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0, (LinearMap.charpoly φ).natTrailingDegree = FiniteDimensional.finrank R M].TFAE
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>IsNoetherian R M<VAR>φ : Module.End R M<GOAL>LinearMap.charpoly φ = Polynomial.X ^ FiniteDimensional.finrank R M ↔ ∀ (m : M), ∃ n, (φ ^ n) m = 0
<VAR>K : Type u_2<VAR>M : Type u_3<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>Module.Finite K M<VAR>φ : Module.End K M<GOAL>[φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < LinearMap.ker φ, ∃ m, m ≠ 0 ∧ φ m = 0].TFAE
<VAR>K : Type u_2<VAR>M : Type u_3<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>Module.Finite K M<VAR>φ : Module.End K M<GOAL>Polynomial.constantCoeff (LinearMap.charpoly φ) = 0 ↔ ∃ m, m ≠ 0 ∧ φ m = 0
<VAR>K : Type u_2<VAR>M : Type u_3<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>Module.Finite K M<VAR>φ : Module.End K M<GOAL>[¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, LinearMap.ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
<VAR>K : Type u_2<VAR>M : Type u_3<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>Module.Finite K M<VAR>φ : Module.End K M<GOAL>FiniteDimensional.finrank K ↥(φ.maxGenEigenspace 0) = (LinearMap.charpoly φ).natTrailingDegree
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>algebraMap K (RatFunc K) = RatFunc.C
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>a : K<GOAL>(algebraMap (Polynomial K) (RatFunc K)) (Polynomial.C a) = RatFunc.C a
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>(algebraMap (Polynomial K) (RatFunc K)).comp Polynomial.C = RatFunc.C
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>r : K<VAR>x : RatFunc K<GOAL>r • x = RatFunc.C r * x
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>(algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = RatFunc.X
<VAR>K : Type u<VAR>Field K<VAR>c : K<GOAL>(RatFunc.C c).num = Polynomial.C c
<VAR>K : Type u<VAR>Field K<VAR>c : K<GOAL>(RatFunc.C c).denom = 1
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.X.num = Polynomial.X
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.X.denom = 1
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.X ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<VAR>x : RatFunc K<VAR>h : Polynomial.eval₂ f a x.denom = 0<GOAL>RatFunc.eval f a x = 0
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<VAR>x : RatFunc K<VAR>h : RatFunc.eval f a x ≠ 0<GOAL>Polynomial.eval₂ f a x.denom ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<VAR>c : K<GOAL>RatFunc.eval f a (RatFunc.C c) = f c
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<GOAL>RatFunc.eval f a RatFunc.X = a
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<GOAL>RatFunc.eval f a 0 = 0
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<GOAL>RatFunc.eval f a 1 = 1
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<VAR>S : Type u_1<VAR>CommSemiring S<VAR>Algebra S (Polynomial K)<VAR>p : S<GOAL>RatFunc.eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<GOAL>RatFunc.eval f a (x + y) = RatFunc.eval f a x + RatFunc.eval f a y
<VAR>K : Type u<VAR>Field K<VAR>L : Type u<VAR>Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<GOAL>RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.eval f a y
<VAR>K : Type u_1<VAR>Field K<GOAL>(Polynomial.idealX K).asIdeal = Ideal.span {Polynomial.X}
<VAR>K : Type u_1<VAR>Field K<GOAL>(Polynomial.idealX K).valuation RatFunc.X = ↑(Multiplicative.ofAdd (-1))
<VAR>K : Type u_1<VAR>Field K<VAR>f : Polynomial K<VAR>g : Polynomial K<VAR>hg : g ≠ 0<GOAL>(Polynomial.idealX K).valuation (RatFunc.mk f g) = (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g
<VAR>K : Type u_1<VAR>Field K<VAR>x : RatFunc K<GOAL>Valued.v x = (Polynomial.idealX K).valuation x
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>IsNoetherian K V ↔ Module.rank K V < ℵ₀
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>s : Set ι<VAR>IsNoetherian K V<VAR>b : Basis (↑s) K V<GOAL>s.Finite
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>IsNoetherian K V<GOAL>↑(IsNoetherian.finsetBasisIndex K V) = Basis.ofVectorSpaceIndex K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>IsNoetherian K V<GOAL>{ x // x ∈ IsNoetherian.finsetBasisIndex K V } = ↑(Basis.ofVectorSpaceIndex K V)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>IsNoetherian K V<GOAL>Set.range ⇑(IsNoetherian.finsetBasis K V) = Basis.ofVectorSpaceIndex K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>IsNoetherian K V ↔ Module.Finite K V
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.Injective Basis.repr
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : M ≃ₗ[R] ι →₀ R<GOAL>⇑{ repr := e } = fun i => e.symm (Finsupp.single i 1)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Nontrivial R<GOAL>Function.Injective ⇑b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>b.repr.symm (Finsupp.single i 1) = b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<VAR>c : R<GOAL>b.repr.symm (Finsupp.single i c) = c • b i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>b.repr (b i) = Finsupp.single i 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i j : ι<VAR>Decidable (i = j)<GOAL>(b.repr (b i)) j = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>v : ι →₀ R<GOAL>b.repr.symm v = (Finsupp.total ι M R ⇑b) v
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>↑b.repr.symm = Finsupp.total ι M R ⇑b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>v : ι →₀ R<GOAL>b.repr ((Finsupp.total ι M R ⇑b) v) = v
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<GOAL>(Finsupp.total ι M R ⇑b) (b.repr x) = x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>LinearMap.range ↑b.repr = Finsupp.supported R R Set.univ
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>m : M<GOAL>m ∈ Submodule.span R (⇑b '' ↑(b.repr m).support)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>s : Set ι<VAR>m : M<VAR>hm : m ∈ Submodule.span R (⇑b '' s)<GOAL>↑(b.repr m).support ⊆ s
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>m : M<VAR>s : Set ι<GOAL>m ∈ Submodule.span R (⇑b '' s) ↔ ↑(b.repr m).support ⊆ s
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Nontrivial R<VAR>i : ι<VAR>s : Set ι<GOAL>b i ∈ Submodule.span R (⇑b '' s) ↔ i ∈ s
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>∀ (a : M), (b.coord i) a = (b.repr a) i
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>x : M<GOAL>(∀ (i : ι), (b.coord i) x = 0) ↔ x = 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>⇑b.sumCoords = fun m => (b.repr m).sum fun x => id
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<GOAL>⇑b.sumCoords = fun m => ∑ᶠ (i : ι), (b.coord i) m
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>Fintype ι<GOAL>⇑b.sumCoords = ⇑(∑ i : ι, b.coord i)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<GOAL>b.sumCoords (b i) = 1
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<VAR>m : M<VAR>r : R<GOAL>r ∣ (b.coord i) (r • m)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>i : ι<VAR>f : ι →₀ R<GOAL>(b.coord i) (b.repr.symm f) = f i