ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹⁰ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>B : Type u<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : FormallyUnramified R A<VAR>inst✝² : FormallyUnramified A B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<VAR>e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)<VAR>this : Algebra A C := (f₁.comp (IsScalarTower.toAlgHom R A B)).toAlgebra<VAR>F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }<GOAL>f₁ = f₂
<VAR>R : Type u<VAR>inst✝¹⁰ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>B : Type u<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : FormallyUnramified R A<VAR>inst✝² : FormallyUnramified A B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<VAR>e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)<VAR>this : Algebra A C := (f₁.comp (IsScalarTower.toAlgHom R A B)).toAlgebra<VAR>F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }<VAR>F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }<GOAL>f₁ = f₂
<VAR>R : Type u<VAR>inst✝¹⁰ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>B : Type u<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : FormallyUnramified R A<VAR>inst✝² : FormallyUnramified A B<VAR>C : Type u<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra R C<VAR>I : Ideal C<VAR>hI : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[R] C<VAR>e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<VAR>e' : f₁.comp (IsScalarTower.toAlgHom R A B) = f₂.comp (IsScalarTower.toAlgHom R A B)<VAR>this : Algebra A C := (f₁.comp (IsScalarTower.toAlgHom R A B)).toAlgebra<VAR>F₁ : B →ₐ[A] C := { toRingHom := f₁.toRingHom, commutes' := ⋯ }<VAR>F₂ : B →ₐ[A] C := { toRingHom := f₂.toRingHom, commutes' := ⋯ }<VAR>x : B<GOAL>F₁ = F₂
<VAR>θ : Angle<GOAL>(↑π + θ).sign = -θ.sign
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<GOAL>addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<GOAL>(∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>h0 : addOrderOf ↑k • ↑k = 0<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>h0 : ∃ n_1, n_1 • p = n • k<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>a : ℤ<VAR>ha : a • p = n • k<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>a : ℤ<VAR>ha : a • p = n • k<VAR>h0 : ↑n ≠ 0<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>a : ℤ<VAR>ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k<VAR>h0 : ↑n ≠ 0<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>a : ℤ<VAR>ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k<VAR>h0 : ↑n ≠ 0<VAR>han : ↑(a % ↑n).toNat = a % ↑n<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<VAR>k : 𝕜<VAR>hk : addOrderOf ↑k = n<VAR>a : ℤ<VAR>ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k<VAR>h0 : ↑n ≠ 0<VAR>han : ↑(a % ↑n).toNat = a % ↑n<VAR>he : ↑(↑(a % ↑n).toNat / ↑n * p) = ↑k<GOAL>∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑k
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<VAR>r : ↑Γ(X, U)<GOAL>U.ι ''ᵁ (↑U).basicOpen (U.topIso.inv r) = X.basicOpen r
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<GOAL>(filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts).card ≤ 2 ^ (F.card - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<GOAL>filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts ⊆ image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<GOAL>∀ ⦃x : Finset α⦄, x ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts → x ∈ image (fun P => filter (fun i => ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x) s) (F.erase t).powerset
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<GOAL>∀ ⦃x : Finset α⦄, ∀ x_1 ∈ x, ∀ x_2 ⊆ F, filter (fun i => ∀ u ∈ F, u ∈ x_2 ↔ i ∈ u) s = x → x ⊆ t → ∀ x_3 ∈ x, ∃ a ⊆ F.erase t, filter (fun i => ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x) s = x
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P✝ : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>i : α<VAR>P : Finset (Finset α)<VAR>PQ : P ⊆ F<VAR>hi : i ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s<VAR>hy₂ : filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s ⊆ t<VAR>j : α<VAR>_hj : j ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s<GOAL>∃ a ⊆ F.erase t, filter (fun i => ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x) s = filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P✝ : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>i : α<VAR>P : Finset (Finset α)<VAR>PQ : P ⊆ F<VAR>hi : i ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s<VAR>hy₂ : filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s ⊆ t<VAR>j : α<VAR>_hj : j ∈ filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s<GOAL>filter (fun i => ∀ x ∈ F, x ∈ insert t (P.erase t) ↔ i ∈ x) s = filter (fun i => ∀ u ∈ F, u ∈ P ↔ i ∈ u) s
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝ : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>(noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝ : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>(noncommPiCoprod ϕ hcomm).range ≤ ⨆ i, (ϕ i).range
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Type u_3<VAR>inst✝ : (i : ι) → Group (H i)<VAR>ϕ : (i : ι) → H i →* G<VAR>f g : (i : ι) → H i<VAR>hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>⨆ i, (ϕ i).range ≤ (noncommPiCoprod ϕ hcomm).range
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<GOAL>ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, dist x a < δ → dist (f x) (f a) < ε
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β✝<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ✝<VAR>μ✝ μ' : Measure α✝<VAR>ν✝ ν' : Measure β✝<VAR>τ✝ : Measure γ✝<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>f : α × β → γ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>τ : Measure γ<VAR>hf : Measurable f<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<VAR>h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ<GOAL>QuasiMeasurePreserving f (μ.prod ν) τ
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β✝<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ✝<VAR>μ✝ μ' : Measure α✝<VAR>ν✝ ν' : Measure β✝<VAR>τ✝ : Measure γ✝<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>f : α × β → γ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>τ : Measure γ<VAR>hf : Measurable f<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<VAR>h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ<GOAL>QuasiMeasurePreserving f (map Prod.swap (ν.prod μ)) τ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>hB : B ⊆ A<VAR>hC : C ⊆ A<VAR>h : A ↓∩ B = A ↓∩ C<GOAL>B = C
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>h : A ↓∩ B = A ↓∩ C<VAR>hB : A ∩ B = B<VAR>hC : A ∩ C = C<GOAL>B = C
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<VAR>hB : A ∩ B = B<VAR>hC : A ∩ C = C<VAR>h : B = C<GOAL>B = C
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝ : CommRing R<VAR>a b c : lib R X<VAR>h : Rel R X b c<GOAL>Rel R X (a - b) (a - c)
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : 0 < n<VAR>div : p ∣ n<GOAL>1 ≤ padicValNat p n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>(mk S.f (Abelian.coimage.π S.g) ⋯).Exact ↔ S.Exact
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>(algebraMap K E) (discr K ⇑pb.basis) = (-1) ^ (n * (n - 1) / 2) * ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)) = (-1) ^ (n * (n - 1) / 2) * ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>(∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1) * ((∏ x : Fin pb.dim, ∏ x_1 ∈ Ioi x, ((e x_1) pb.gen - (e x) pb.gen)) * ∏ x : Fin pb.dim, ∏ x_1 ∈ Ioi x, ((e x) pb.gen - (e x_1) pb.gen)) = (-1) ^ (n * (n - 1) / 2) * ((∏ x : Fin pb.dim, ∏ x_1 ∈ Ioi x, ((e x_1) pb.gen - (e x) pb.gen)) * ∏ x : Fin pb.dim, ∏ x_1 ∈ Ioi x, ((e x) pb.gen - (e x_1) pb.gen))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1 = (-1) ^ (n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>(-1) ^ ∑ i : Fin pb.dim, (Ioi i).card = (-1) ^ (n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>∑ i : Fin pb.dim, (Ioi i).card = n * (n - 1) / 2
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>∑ x : Fin pb.dim, ↑(Ioi x).card = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<GOAL>∑ x : Fin pb.dim, ↑(Ioi x).card = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<GOAL>∑ x : Fin pb.dim, ↑(pb.dim - (↑x + 1)) = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<GOAL>↑pb.dim * ↑pb.dim - (∑ x : Fin pb.dim, ↑↑x + ↑pb.dim) = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<GOAL>↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<VAR>hn : n = pb.dim<GOAL>↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<VAR>hn : n = pb.dim<VAR>h₂ : 2 ∣ pb.dim * (pb.dim - 1)<GOAL>↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<VAR>hn : n = pb.dim<VAR>h₂ : 2 ∣ pb.dim * (pb.dim - 1)<VAR>hne : ↑2 ≠ 0<GOAL>↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<VAR>hn : n = pb.dim<VAR>h₂ : 2 ∣ pb.dim * (pb.dim - 1)<VAR>hne : ↑2 ≠ 0<VAR>hle : 1 ≤ pb.dim<GOAL>↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)