ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<GOAL>p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<GOAL>p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n) = p ^ n.succ * r
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>(algebraMap R K) (Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n)) = (algebraMap R K) (p ^ n.succ * r)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>(algebraMap R K) (Q.coeff 0) ^ n.succ * ((-1) ^ (n.succ * n) * (algebraMap R K) ((minpoly R B.gen).coeff 0) ^ n) = (algebraMap R K) p ^ n.succ * (algebraMap R K) r
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>(algebraMap R K) (Q.coeff 0) ^ n.succ * ((-1) ^ (n.succ * n) * (algebraMap R K) ((minpoly R B.gen).coeff 0) ^ n) = (Algebra.norm K) (Q.coeff 0 • B.gen ^ n)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>Q.coeff 0 • B.gen ^ n + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n) = p • (z * B.gen ^ n)
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>(Algebra.norm K) (p • (z * B.gen ^ n) - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) = (algebraMap R K) p ^ n.succ * (algebraMap R K) r
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>Q.coeff 0 • B.gen ^ n + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n) = (Q.coeff 0 • 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<VAR>aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n<VAR>hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<VAR>r : R<VAR>hr : (algebraMap R K) r = (Algebra.norm K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))<GOAL>(Q.coeff 0 • B.gen ^ 0 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n = (aeval B.gen) Q * B.gen ^ n
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<GOAL>|truncation f A x| ≤ |A|
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<GOAL>|if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>a : Equalizer.Presieve.Arrows.FirstObj F X<VAR>i j : α<GOAL>Pi.π (fun ij => F.obj (op (pullback (c.inj ij.1) (c.inj ij.2)))) (i, j) (Equalizer.Presieve.Arrows.firstMap F X c.inj a) = Pi.π (fun ij => F.obj (op (pullback (c.inj ij.1) (c.inj ij.2)))) (i, j) (Equalizer.Presieve.Arrows.secondMap F X c.inj a)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>a : Equalizer.Presieve.Arrows.FirstObj F X<VAR>i j : α<GOAL>F.map (pullback.fst (c.inj i) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) i a) = F.map (pullback.snd (c.inj i) (c.inj j)).op (Pi.π (fun i => F.obj (op (X i))) j a)
<VAR>o : Ordinal.{u_1}<GOAL>(nim o).LeftMoves = (Quotient.out o).α
<VAR>o : Ordinal.{u_1}<GOAL>(mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).LeftMoves = (Quotient.out o).α
<VAR>n p : ℕ<GOAL>(↑p + 1) * ∑ k ∈ range n, ↑k ^ p = eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ
<VAR>n p : ℕ<GOAL>∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) = ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) - _root_.bernoulli p.succ
<VAR>n p : ℕ<GOAL>↑p + 1 ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<GOAL>P.toPoly.degree ≤ 1
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>↑m < lift.{u, v} x ↔ ↑m < x
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>IsUnit ((X.toToΓSpecMapBasicOpen r) r)
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>(X.toToΓSpecMapBasicOpen r) r = (X.presheaf.map (eqToHom ⋯).op) ((X.toRingedSpace.presheaf.map (homOfLE ⋯).op) r)
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>(X.toToΓSpecMapBasicOpen r) r = (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : ℝ → E<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>hg : MellinConvergent g s<GOAL>MellinConvergent (fun t => f t + g t) s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : ℝ → E<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>hg : MellinConvergent g s<GOAL>mellin (fun t => f t + g t) s = mellin f s + mellin g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ x : Fin n → ℕ<VAR>hx : x ∈ ↑(sphere n d k)<GOAL>x ∈ (fun x => (WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 √↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n : ℕ<VAR>hf : IsPeriodicPt f n x<VAR>m : ℕ<GOAL>IsPeriodicPt f^[m] n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n : ℕ<VAR>hf : IsPeriodicPt f n x<VAR>m : ℕ<GOAL>IsFixedPt f^[n]^[m] x
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>t : W<VAR>ht : t ∈ cs.leftInvSeq ω<GOAL>cs.IsReflection t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>t : W<VAR>ht : t ∈ cs.rightInvSeq ω.reverse<GOAL>cs.IsReflection t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>f : Arrow C<VAR>inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>x y : SimplexCategory<VAR>g : x ⟶ y<VAR>j : Fin (x.len + 1)<GOAL>f.hom ≫ (fun i => WidePushout.ι (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g) i)) j = WidePushout.head fun x => f.hom
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>inst✝ : ClosedUnderIsomorphisms Q<VAR>h : P ≤ Q<GOAL>isoClosure Q ≤ Q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddGroup G<VAR>f : α →₀ G<VAR>a a' : α<GOAL>(erase a f) a' = (f - single a (f a)) a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddGroup G<VAR>f : α →₀ G<VAR>a : α<GOAL>(erase a f) a = (f - single a (f a)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddGroup G<VAR>f : α →₀ G<VAR>a a' : α<VAR>h : a ≠ a'<GOAL>(erase a f) a' = (f - single a (f a)) a'
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>x : E<GOAL>x ∈ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y Z X X' : C<VAR>f : X ⟶ X'<GOAL>f = (λ_ X).inv ≫ 𝟙_ C ◁ f ≫ (λ_ X').hom
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<GOAL>Submartingale (f - g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Supermartingale g ℱ μ<GOAL>Submartingale (f + -g) ℱ μ
<VAR>α✝ : Type ua<VAR>β : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>ι : Sort u_2<VAR>α : Type u_3<VAR>γ : Type u_4<VAR>u : ι → UniformSpace γ<VAR>f : α → γ<GOAL>𝓤 α = 𝓤 α
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ ψ : W.LeftFraction₂ X Y<GOAL>φ.fst.map L ⋯ = ψ.fst.map L ⋯ ∧ φ.snd.map L ⋯ = ψ.snd.map L ⋯ ↔ LeftFraction₂Rel φ ψ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ ψ : W.LeftFraction₂ X Y<GOAL>LeftFractionRel φ.fst ψ.fst ∧ LeftFractionRel φ.snd ψ.snd ↔ LeftFraction₂Rel φ ψ