ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<GOAL>LinearMap.range g.toLinearPMap.toFun = Submodule.map (LinearMap.snd R E F) g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<GOAL>f.inverse.domain = LinearMap.range f.toFun
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>x : F × E<VAR>hv : x ∈ Submodule.map (LinearEquiv.prodComm R E F) f.graph<VAR>hv' : x.1 = 0<GOAL>x.2 = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<GOAL>f.inverse.graph = Submodule.map (LinearEquiv.prodComm R E F) f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<GOAL>LinearMap.range f.inverse.toFun = f.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>x : ↥f.domain<GOAL>(↑f x, ↑x) ∈ f.inverse.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>y : ↥f.inverse.domain<VAR>x : ↥f.domain<VAR>hxy : ↑f x = ↑y<GOAL>↑f.inverse y = ↑x
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>σ τ : p.Gal<VAR>h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x<GOAL>σ = τ
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Fact (Polynomial.Splits (algebraMap F E) p)<VAR>Normal F E<GOAL>Function.Surjective ⇑(Polynomial.Gal.restrict p E)
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>h : Fact (Polynomial.Splits (algebraMap F E) p)<GOAL>Function.Bijective (Polynomial.Gal.mapRoots p E)
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Fact (Polynomial.Splits (algebraMap F E) p)<VAR>ϕ : p.Gal<VAR>x : ↑(p.rootSet E)<GOAL>ϕ • x = (Polynomial.Gal.rootsEquivRoots p E) (ϕ • (Polynomial.Gal.rootsEquivRoots p E).symm x)
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Fact (Polynomial.Splits (algebraMap F E) p)<VAR>hp : Irreducible p<GOAL>MulAction.IsPretransitive p.Gal ↑(p.rootSet E)
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Fact (Polynomial.Splits (algebraMap F E) p)<VAR>ϕ : E ≃ₐ[F] E<VAR>x : ↑(p.rootSet E)<GOAL>↑((Polynomial.Gal.restrict p E) ϕ • x) = ϕ ↑x
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Fact (Polynomial.Splits (algebraMap F E) p)<VAR>ϕ : E ≃ₐ[F] E<VAR>x : ↑(p.rootSet E)<GOAL>↑(((Polynomial.Gal.galActionHom p E) ((Polynomial.Gal.restrict p E) ϕ)) x) = ϕ ↑x
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Fact (Polynomial.Splits (algebraMap F E) p)<GOAL>Function.Injective ⇑(Polynomial.Gal.galActionHom p E)
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<VAR>Decidable (q = 0)<VAR>hpq : p ∣ q<GOAL>Polynomial.Gal.restrictDvd hpq = if hq : q = 0 then 1 else Polynomial.Gal.restrict p q.SplittingField
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<VAR>hpq : p ∣ q<VAR>hq : q ≠ 0<GOAL>Function.Surjective ⇑(Polynomial.Gal.restrictDvd hpq)
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<GOAL>Function.Injective ⇑(Polynomial.Gal.restrictProd p q)
<VAR>F : Type u_1<VAR>Field F<VAR>p₁ q₁ p₂ q₂ : F[X]<VAR>hq₁ : q₁ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h₁ : Polynomial.Splits (algebraMap F q₁.SplittingField) p₁<VAR>h₂ : Polynomial.Splits (algebraMap F q₂.SplittingField) p₂<GOAL>Polynomial.Splits (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂)
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<VAR>hq : q.natDegree ≠ 0<GOAL>Polynomial.Splits (algebraMap F (p.comp q).SplittingField) p
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<VAR>hq : q.natDegree ≠ 0<GOAL>Function.Surjective ⇑(Polynomial.Gal.restrictComp p q hq)
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>hp : p.Separable<GOAL>Fintype.card p.Gal = FiniteDimensional.finrank F p.SplittingField
<VAR>F : Type u_1<VAR>Field F<VAR>p : F[X]<VAR>CharZero F<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<GOAL>p.natDegree ∣ Fintype.card p.Gal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>CommRing L<VAR>Nontrivial L<VAR>Algebra R L<VAR>Algebra S L<VAR>Algebra K L<VAR>IsScalarTower R K L<VAR>IsScalarTower R S L<VAR>IsIntegrallyClosed R<VAR>IsDomain S<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>minpoly K ((algebraMap S L) s) = Polynomial.map (algebraMap R K) (minpoly R s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsIntegrallyClosed R<VAR>IsDomain S<VAR>Algebra K S<VAR>IsScalarTower R K S<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>minpoly K s = Polynomial.map (algebraMap R K) (minpoly R s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp : (Polynomial.aeval s) p = 0<GOAL>minpoly R s ∣ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<GOAL>(Polynomial.aeval s) p = 0 ↔ minpoly R s ∣ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<GOAL>RingHom.ker (Polynomial.aeval s).toRingHom = Ideal.span {minpoly R s}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : (Polynomial.aeval s) p = 0<GOAL>(minpoly R s).degree ≤ p.degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<GOAL>P = minpoly R s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>Prime (minpoly R x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>Function.Injective ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a : AdjoinRoot (minpoly R x)<GOAL>(minpoly.equivAdjoin hx) a = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {minpoly R x})) ↑(Polynomial.eval₂RingHom (algebraMap R ↥(Algebra.adjoin R {x})) ⟨x, ⋯⟩) ⋯) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>b : ↥(Algebra.adjoin R {x})<GOAL>(minpoly.equivAdjoin hx).symm b = Function.surjInv ⋯ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>(Algebra.adjoin.powerBasis' hx).dim = (minpoly R x).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>(Algebra.adjoin.powerBasis' hx).gen = ⟨x, ⋯⟩
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>B : PowerBasis R S<VAR>hint : IsIntegral R x<VAR>hx : B.gen ∈ Algebra.adjoin R {x}<GOAL>(B.ofGenMemAdjoin' hint hx).dim = (minpoly R x).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>IsDomain R<VAR>Algebra R S<VAR>IsDomain S<VAR>NoZeroSMulDivisors R S<VAR>IsIntegrallyClosed R<VAR>x : S<VAR>B : PowerBasis R S<VAR>hint : IsIntegral R x<VAR>hx : B.gen ∈ Algebra.adjoin R {x}<GOAL>(B.ofGenMemAdjoin' hint hx).gen = x
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>minpolyDiv R x * (Polynomial.X - Polynomial.C x) = Polynomial.map (algebraMap R S) (minpoly R x)
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>i : ℕ<GOAL>(minpolyDiv R x).coeff i = (algebraMap R S) ((minpoly R x).coeff (i + 1)) + (minpolyDiv R x).coeff (i + 1) * x
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<VAR>Nontrivial S<GOAL>minpolyDiv R x ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : ¬IsIntegral R x<GOAL>minpolyDiv R x = 0
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>(minpolyDiv R x).Monic
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>Polynomial.eval x (minpolyDiv R x) = (Polynomial.aeval x) (Polynomial.derivative (minpoly R x))
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>IsDomain S<VAR>y : S<VAR>hxy : y ≠ x<VAR>hy : (Polynomial.aeval y) (minpoly R x) = 0<GOAL>Polynomial.eval y (minpolyDiv R x) = 0
<VAR>R : Type u_3<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>IsDomain T<VAR>DecidableEq T<VAR>x : S<VAR>y : T<VAR>σ : S →+* T<VAR>hy : Polynomial.eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0<GOAL>Polynomial.eval₂ σ y (minpolyDiv R x) = if σ x = y then σ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>IsDomain T<VAR>DecidableEq T<VAR>x : S<VAR>σ₁ σ₂ : S →ₐ[R] T<GOAL>Polynomial.eval₂ (↑σ₁) (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>IsDomain S<VAR>DecidableEq S<VAR>y : S<VAR>hy : (Polynomial.aeval y) (minpoly R x) = 0<GOAL>Polynomial.eval y (minpolyDiv R x) = if x = y then (Polynomial.aeval x) (Polynomial.derivative (minpoly R x)) else 0
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<VAR>Nontrivial S<GOAL>(minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>(minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<VAR>Nontrivial S<GOAL>(minpolyDiv R x).natDegree < (minpoly R x).natDegree
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>i : ℕ<GOAL>(minpolyDiv R x).coeff i ∈ Algebra.adjoin R {x}
<VAR>R : Type u_1<VAR>K : Type u_3<VAR>S : Type u_2<VAR>CommRing R<VAR>Field K<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<VAR>IsDomain R<VAR>IsIntegrallyClosed R<VAR>IsDomain S<VAR>Algebra R K<VAR>Algebra K S<VAR>IsScalarTower R K S<VAR>IsFractionRing R K<GOAL>minpolyDiv R x = minpolyDiv K x
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<VAR>i : ℕ<VAR>hi : i ≤ (minpolyDiv R x).natDegree<GOAL>(minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈ Submodule.span R ((fun x_1 => x ^ x_1) '' Set.Iio i)
<VAR>R : Type u_2<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>Submodule.span R (Set.range (minpolyDiv R x).coeff) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : Type u_1<VAR>Field E<VAR>Algebra K E<VAR>IsAlgClosed E<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>x : L<VAR>hxL : Algebra.adjoin K {x} = ⊤<VAR>r : ℕ<VAR>hr : r < FiniteDimensional.finrank K L<GOAL>∑ σ : L →ₐ[K] E, Polynomial.map (↑σ) ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) • minpolyDiv K x) = Polynomial.X ^ r
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<GOAL>∀ (a a_1 : ℕ × K), PerfectClosure.R K p a a_1 ↔ ∃ n x, a = (n, x) ∧ a_1 = (n + 1, (frobenius K p) x)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<GOAL>Function.Surjective (PerfectClosure.mk K p)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>m : ℕ<VAR>x : K<GOAL>PerfectClosure.mk K p (m + 1, x ^ p) = PerfectClosure.mk K p (m, x)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : ℕ × K<GOAL>Quot.mk (PerfectClosure.R K p) x = PerfectClosure.mk K p x
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>L : Type u_1<VAR>f : ℕ × K → L<VAR>hf : ∀ (x y : ℕ × K), PerfectClosure.R K p x y → f x = f y<VAR>x : ℕ × K<GOAL>(PerfectClosure.mk K p x).liftOn f hf = f x
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : PerfectClosure K p<VAR>q : PerfectClosure K p → Prop<VAR>h : ∀ (x : ℕ × K), q (PerfectClosure.mk K p x)<GOAL>q x
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x1 x2 y : ℕ × K<VAR>H : PerfectClosure.R K p x1 x2<GOAL>PerfectClosure.mk K p (x1.1 + y.1, (⇑(frobenius K p))^[y.1] x1.2 * (⇑(frobenius K p))^[x1.1] y.2) = PerfectClosure.mk K p (x2.1 + y.1, (⇑(frobenius K p))^[y.1] x2.2 * (⇑(frobenius K p))^[x2.1] y.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y1 y2 : ℕ × K<VAR>H : PerfectClosure.R K p y1 y2<GOAL>PerfectClosure.mk K p (x.1 + y1.1, (⇑(frobenius K p))^[y1.1] x.2 * (⇑(frobenius K p))^[x.1] y1.2) = PerfectClosure.mk K p (x.1 + y2.1, (⇑(frobenius K p))^[y2.1] x.2 * (⇑(frobenius K p))^[x.1] y2.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y : ℕ × K<GOAL>PerfectClosure.mk K p x * PerfectClosure.mk K p y = PerfectClosure.mk K p (x.1 + y.1, (⇑(frobenius K p))^[y.1] x.2 * (⇑(frobenius K p))^[x.1] y.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<GOAL>1 = PerfectClosure.mk K p (0, 1)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x1 x2 y : ℕ × K<VAR>H : PerfectClosure.R K p x1 x2<GOAL>PerfectClosure.mk K p (x1.1 + y.1, (⇑(frobenius K p))^[y.1] x1.2 + (⇑(frobenius K p))^[x1.1] y.2) = PerfectClosure.mk K p (x2.1 + y.1, (⇑(frobenius K p))^[y.1] x2.2 + (⇑(frobenius K p))^[x2.1] y.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y1 y2 : ℕ × K<VAR>H : PerfectClosure.R K p y1 y2<GOAL>PerfectClosure.mk K p (x.1 + y1.1, (⇑(frobenius K p))^[y1.1] x.2 + (⇑(frobenius K p))^[x.1] y1.2) = PerfectClosure.mk K p (x.1 + y2.1, (⇑(frobenius K p))^[y2.1] x.2 + (⇑(frobenius K p))^[x.1] y2.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y : ℕ × K<GOAL>PerfectClosure.mk K p x + PerfectClosure.mk K p y = PerfectClosure.mk K p (x.1 + y.1, (⇑(frobenius K p))^[y.1] x.2 + (⇑(frobenius K p))^[x.1] y.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : ℕ × K<GOAL>-PerfectClosure.mk K p x = PerfectClosure.mk K p (x.1, -x.2)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<GOAL>0 = PerfectClosure.mk K p (0, 0)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<GOAL>PerfectClosure.mk K p (0, 0) = 0
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>n : ℕ<GOAL>PerfectClosure.mk K p (n, 0) = 0
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>m n : ℕ<VAR>x y : K<VAR>H : (⇑(frobenius K p))^[m] x = y<GOAL>PerfectClosure.mk K p (n, x) = PerfectClosure.mk K p (m + n, y)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y : ℕ × K<GOAL>PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : ℕ × K<VAR>n : ℕ<GOAL>PerfectClosure.mk K p x ^ n = PerfectClosure.mk K p (x.1, x.2 ^ n)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>n x : ℕ<GOAL>↑x = PerfectClosure.mk K p (n, ↑x)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : ℤ<GOAL>↑x = PerfectClosure.mk K p (0, ↑x)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y : ℕ<GOAL>↑x = ↑y ↔ ↑x = ↑y
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : ℕ × K<GOAL>(frobenius (PerfectClosure K p) p) (PerfectClosure.mk K p x) = PerfectClosure.mk K p (x.1, x.2 ^ p)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : K<GOAL>(PerfectClosure.of K p) x = PerfectClosure.mk K p (0, x)
<VAR>K : Type u<VAR>CommRing K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>n : ℕ<VAR>x : K<GOAL>(⇑(frobenius (PerfectClosure K p) p))^[n] (PerfectClosure.mk K p (n, x)) = (PerfectClosure.of K p) x
<VAR>K : Type u<VAR>CommRing K<VAR>IsReduced K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x y : ℕ × K<GOAL>PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔ (⇑(frobenius K p))^[y.1] x.2 = (⇑(frobenius K p))^[x.1] y.2
<VAR>K : Type u<VAR>Field K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>x : ℕ × K<GOAL>(PerfectClosure.mk K p x)⁻¹ = PerfectClosure.mk K p (x.1, x.2⁻¹)
<VAR>F : Type u_1<VAR>Field F<VAR>Finite F<VAR>Algebra (ZMod (ringChar F)) F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pnz : p ≠ 0<VAR>hp : (Polynomial.aeval x) p = 0<GOAL>(minpoly A x).degree ≤ p.degree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>e : B<VAR>FiniteDimensional A B<GOAL>minpoly A e ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<GOAL>p = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>hp : (Polynomial.aeval x) p = 0<GOAL>minpoly A x ∣ p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>p : A[X]<GOAL>minpoly A x ∣ p ↔ (Polynomial.aeval x) p = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>IsReduced B<GOAL>IsRadical (minpoly A x)
<VAR>A : Type u_3<VAR>K : Type u_4<VAR>R : Type u_5<VAR>CommRing A<VAR>Field K<VAR>CommRing R<VAR>Algebra A K<VAR>Algebra A R<VAR>Algebra K R<VAR>IsScalarTower A K R<VAR>x : R<GOAL>minpoly K x ∣ Polynomial.map (algebraMap A K) (minpoly A x)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>K : Type u_5<VAR>L : Type u_6<VAR>CommRing R<VAR>CommRing S<VAR>Field K<VAR>CommRing L<VAR>Algebra R S<VAR>Algebra R K<VAR>Algebra S L<VAR>Algebra K L<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>IsScalarTower R S L<VAR>s : S<GOAL>minpoly K ((algebraMap S L) s) ∣ Polynomial.map (algebraMap R K) (minpoly R s)
<VAR>R : Type u_3<VAR>K : Type u_4<VAR>T : Type u_5<VAR>U : Type u_6<VAR>CommRing R<VAR>Field K<VAR>CommRing T<VAR>Algebra R K<VAR>Algebra K T<VAR>Algebra R T<VAR>IsScalarTower R K T<VAR>CommSemiring U<VAR>Algebra K U<VAR>Algebra R U<VAR>IsScalarTower R K U<VAR>x : T<VAR>y : U<VAR>hy : (Polynomial.aeval y) (minpoly K x) = 0<GOAL>(Polynomial.aeval y) (minpoly R x) = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<GOAL>RingHom.ker (Polynomial.aeval x) = Submodule.span A[X] {minpoly A x}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<VAR>hp3 : p.Monic<GOAL>p = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<VAR>p : A[X]<VAR>hp1 : Irreducible p<VAR>hp2 : (Polynomial.aeval x) p = 0<GOAL>p * Polynomial.C p.leadingCoeff⁻¹ = minpoly A x
<VAR>A : Type u_1<VAR>Field A<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>a : A<GOAL>minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X - Polynomial.C a)
<VAR>A : Type u_1<VAR>Field A<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>a : A<GOAL>minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X + Polynomial.C a)
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>K : Type u_5<VAR>Field F<VAR>Ring E<VAR>CommRing K<VAR>IsDomain K<VAR>Algebra F E<VAR>Algebra F K<VAR>FiniteDimensional F E<GOAL>Function.Injective (minpoly.rootsOfMinPolyPiType F E K)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>Nontrivial B<VAR>a : A<GOAL>minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a
<VAR>A : Type u_1<VAR>Field A<VAR>a : A<GOAL>minpoly A a = Polynomial.X - Polynomial.C a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>Nontrivial B<GOAL>minpoly A 0 = Polynomial.X
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>Algebra A B<VAR>Nontrivial B<GOAL>minpoly A 1 = Polynomial.X - 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>IsDomain B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<GOAL>Prime (minpoly A x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>IsDomain B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>y : A<VAR>h : (minpoly A x).IsRoot y<GOAL>(algebraMap A B) y = x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>IsDomain B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<GOAL>(minpoly A x).coeff 0 = 0 ↔ x = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Field A<VAR>Ring B<VAR>IsDomain B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>h : x ≠ 0<GOAL>(minpoly A x).coeff 0 ≠ 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>σ : L ≃ₐ[K] L<VAR>hσ : IsOfFinOrder σ<GOAL>minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>σ : L →ₐ[K] L<VAR>hσ : IsOfFinOrder σ<GOAL>minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1
<VAR>k : Type u<VAR>Field k<VAR>self : IsAlgClosed k<VAR>p : k[X]<GOAL>Polynomial.Splits (RingHom.id k) p
<VAR>k : Type u_1<VAR>K : Type u_2<VAR>Field k<VAR>IsAlgClosed k<VAR>Field K<VAR>f : K →+* k<VAR>p : K[X]<GOAL>Polynomial.Splits f p
<VAR>k : Type u_1<VAR>K : Type u_2<VAR>Field k<VAR>IsAlgClosed k<VAR>Field K<VAR>f : k →+* K<VAR>p : k[X]<GOAL>Polynomial.Splits f p
<VAR>k : Type u<VAR>Field k<VAR>IsAlgClosed k<VAR>p : k[X]<VAR>hp : p.degree ≠ 0<GOAL>∃ x, p.IsRoot x