[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
⊢ discr A b = det (traceMatrix A b)
[PROOFSTEP]
unfold discr
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
⊢ det (traceMatrix A b) = det (traceMatrix A b)
[PROOFSTEP]
convert rfl
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : CommRing C
inst✝³ : Algebra A C
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (↑b ∘ ↑f.symm) = discr A ↑b
[PROOFSTEP]
classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : CommRing C
inst✝³ : Algebra A C
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (↑b ∘ ↑f.symm) = discr A ↑b
[PROOFSTEP]
rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0
[PROOFSTEP]
classical
obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
have : (traceMatrix A b).mulVec g = 0 := by
  ext i
  have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by intro j; simp [mul_comm]
  simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j => this j, ←
    LinearMap.map_sum, ← sum_mul, hg, zero_mul, LinearMap.map_zero]
by_contra h
rw [discr_def] at h
simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0
[PROOFSTEP]
obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
[GOAL]
case intro.intro.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ discr A b = 0
[PROOFSTEP]
have : (traceMatrix A b).mulVec g = 0 := by
  ext i
  have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by intro j; simp [mul_comm]
  simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j => this j, ←
    LinearMap.map_sum, ← sum_mul, hg, zero_mul, LinearMap.map_zero]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ mulVec (traceMatrix A b) g = 0
[PROOFSTEP]
ext i
[GOAL]
case h
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ mulVec (traceMatrix A b) g i = OfNat.ofNat 0 i
[PROOFSTEP]
have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by intro j; simp [mul_comm]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ ∀ (j : ι), ↑(trace A B) (b i * b j) * g j = ↑(trace A B) (g j • b j * b i)
[PROOFSTEP]
intro j
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i j : ι
⊢ ↑(trace A B) (b i * b j) * g j = ↑(trace A B) (g j • b j * b i)
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case h
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
this : ∀ (j : ι), ↑(trace A B) (b i * b j) * g j = ↑(trace A B) (g j • b j * b i)
⊢ mulVec (traceMatrix A b) g i = OfNat.ofNat 0 i
[PROOFSTEP]
simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j => this j, ← LinearMap.map_sum,
  ← sum_mul, hg, zero_mul, LinearMap.map_zero]
[GOAL]
case intro.intro.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : mulVec (traceMatrix A b) g = 0
⊢ discr A b = 0
[PROOFSTEP]
by_contra h
[GOAL]
case intro.intro.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : mulVec (traceMatrix A b) g = 0
h : ¬discr A b = 0
⊢ False
[PROOFSTEP]
rw [discr_def] at h
[GOAL]
case intro.intro.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : mulVec (traceMatrix A b) g = 0
h : ¬det (traceMatrix A b) = 0
⊢ False
[PROOFSTEP]
simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : CommRing C
inst✝³ : Algebra A C
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : ι → B
P : Matrix ι ι A
⊢ discr A (vecMul b (Matrix.map P ↑(algebraMap A B))) = det P ^ 2 * discr A b
[PROOFSTEP]
rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ← mul_assoc, discr_def, pow_two]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : CommRing C
inst✝³ : Algebra A C
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : ι → B
P : Matrix ι ι A
⊢ discr A (mulVec (Matrix.map P ↑(algebraMap A B)) b) = det P ^ 2 * discr A b
[PROOFSTEP]
rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ← mul_assoc, discr_def, pow_two]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
⊢ discr K ↑b ≠ 0
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : IsEmpty ι
⊢ discr K ↑b ≠ 0
[PROOFSTEP]
have : det (traceMatrix K ↑b) ≠ 0 := by simp
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : IsEmpty ι
⊢ det (traceMatrix K ↑b) ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inl
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : IsEmpty ι
this : det (traceMatrix K ↑b) ≠ 0
⊢ discr K ↑b ≠ 0
[PROOFSTEP]
unfold discr
[GOAL]
case inl
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : IsEmpty ι
this : det (traceMatrix K ↑b) ≠ 0
⊢ det (traceMatrix K ↑b) ≠ 0
[PROOFSTEP]
convert this
[GOAL]
case inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : Nonempty ι
⊢ discr K ↑b ≠ 0
[PROOFSTEP]
have := span_eq_top_of_linearIndependent_of_card_eq_finrank b.linearIndependent (finrank_eq_card_basis b).symm
[GOAL]
case inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : Nonempty ι
this : Submodule.span K (Set.range ↑b) = ⊤
⊢ discr K ↑b ≠ 0
[PROOFSTEP]
classical
rw [discr_def, traceMatrix]
simp_rw [← Basis.mk_apply b.linearIndependent this.ge]
rw [← traceMatrix, traceMatrix_of_basis, ← BilinForm.nondegenerate_iff_det_ne_zero]
exact traceForm_nondegenerate _ _
[GOAL]
case inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : Nonempty ι
this : Submodule.span K (Set.range ↑b) = ⊤
⊢ discr K ↑b ≠ 0
[PROOFSTEP]
rw [discr_def, traceMatrix]
[GOAL]
case inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : Nonempty ι
this : Submodule.span K (Set.range ↑b) = ⊤
⊢ det (↑of fun i j => BilinForm.bilin (traceForm K L) (↑b i) (↑b j)) ≠ 0
[PROOFSTEP]
simp_rw [← Basis.mk_apply b.linearIndependent this.ge]
[GOAL]
case inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : Nonempty ι
this : Submodule.span K (Set.range ↑b) = ⊤
⊢ det
      (↑of fun i j =>
        BilinForm.bilin (traceForm K L)
          (↑(Basis.mk (_ : LinearIndependent K ↑b) (_ : ⊤ ≤ Submodule.span K (Set.range ↑b))) i)
          (↑(Basis.mk (_ : LinearIndependent K ↑b) (_ : ⊤ ≤ Submodule.span K (Set.range ↑b))) j)) ≠
    0
[PROOFSTEP]
rw [← traceMatrix, traceMatrix_of_basis, ← BilinForm.nondegenerate_iff_det_ne_zero]
[GOAL]
case inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
inst✝ : IsSeparable K L
b : Basis ι K L
h✝ : Nonempty ι
this : Submodule.span K (Set.range ↑b) = ⊤
⊢ BilinForm.Nondegenerate (traceForm K L)
[PROOFSTEP]
exact traceForm_nondegenerate _ _
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ ↑(algebraMap K E) (discr K b) = det (embeddingsMatrixReindex K E b e) ^ 2
[PROOFSTEP]
rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply, traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul,
  det_transpose, pow_two]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : IsSeparable K L
⊢ ↑(algebraMap K E) (discr K ↑pb.basis) = ∏ i : Fin pb.dim, ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2
[PROOFSTEP]
rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e, embeddingsMatrixReindex_eq_vandermonde, det_transpose,
  det_vandermonde, ← prod_pow]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : IsSeparable K L
⊢ ∏ x : Fin pb.dim, (∏ j in Ioi x, (↑(↑e j) pb.gen - ↑(↑e x) pb.gen)) ^ 2 =
    ∏ i : Fin pb.dim, ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2
[PROOFSTEP]
congr
[GOAL]
case e_f
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : IsSeparable K L
⊢ (fun x => (∏ j in Ioi x, (↑(↑e j) pb.gen - ↑(↑e x) pb.gen)) ^ 2) = fun i =>
    ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2
[PROOFSTEP]
ext i
[GOAL]
case e_f.h
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : IsSeparable K L
i : Fin pb.dim
⊢ (∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen)) ^ 2 = ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2
[PROOFSTEP]
rw [← prod_pow]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ↑(algebraMap K E) (discr K ↑pb.basis) =
    ∏ i : Fin pb.dim, ∏ j in Ioi i, -((↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen))
[PROOFSTEP]
rw [discr_powerBasis_eq_prod _ _ _ e]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∏ i : Fin pb.dim, ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2 =
    ∏ i : Fin pb.dim, ∏ j in Ioi i, -((↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen))
[PROOFSTEP]
congr
[GOAL]
case e_f
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (fun i => ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2) = fun i =>
    ∏ j in Ioi i, -((↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen))
[PROOFSTEP]
ext i
[GOAL]
case e_f.h
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
⊢ ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2 =
    ∏ j in Ioi i, -((↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen))
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_f
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
⊢ (fun j => (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2) = fun j =>
    -((↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen))
[PROOFSTEP]
ext j
[GOAL]
case e_f.h.e_f.h
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i j : Fin pb.dim
⊢ (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) ^ 2 = -((↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen))
[PROOFSTEP]
ring
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ↑(algebraMap K E) (discr K ↑pb.basis) =
    (-1) ^ (n * (n - 1) / 2) *
      ∏ i : Fin pb.dim, ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen)
[PROOFSTEP]
rw [discr_powerBasis_eq_prod' _ _ _ e]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∏ i : Fin pb.dim, ∏ j in 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 in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen)
[PROOFSTEP]
simp_rw [fun i j => neg_eq_neg_one_mul ((e j pb.gen - e i pb.gen) * (e i pb.gen - e j pb.gen)), prod_mul_distrib]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (∏ x : Fin pb.dim, ∏ x in Ioi x, -1) *
      ((∏ x : Fin pb.dim, ∏ x_1 in Ioi x, (↑(↑e x_1) pb.gen - ↑(↑e x) pb.gen)) *
        ∏ x : Fin pb.dim, ∏ x_1 in Ioi x, (↑(↑e x) pb.gen - ↑(↑e x_1) pb.gen)) =
    (-1) ^ (n * (n - 1) / 2) *
      ((∏ x : Fin pb.dim, ∏ x_1 in Ioi x, (↑(↑e x_1) pb.gen - ↑(↑e x) pb.gen)) *
        ∏ x : Fin pb.dim, ∏ x_1 in Ioi x, (↑(↑e x) pb.gen - ↑(↑e x_1) pb.gen))
[PROOFSTEP]
congr
[GOAL]
case e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∏ x : Fin pb.dim, ∏ x in Ioi x, -1 = (-1) ^ (n * (n - 1) / 2)
[PROOFSTEP]
simp only [prod_pow_eq_pow_sum, prod_const]
[GOAL]
case e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (-1) ^ ∑ x : Fin pb.dim, Finset.card (Ioi x) = (-1) ^ (n * (n - 1) / 2)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∑ x : Fin pb.dim, Finset.card (Ioi x) = n * (n - 1) / 2
[PROOFSTEP]
rw [← @Nat.cast_inj ℚ, Nat.cast_sum]
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∑ x : Fin pb.dim, ↑(Finset.card (Ioi x)) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
have : ∀ x : Fin pb.dim, ↑x + 1 ≤ pb.dim := by simp [Nat.succ_le_iff, Fin.is_lt]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
[PROOFSTEP]
simp [Nat.succ_le_iff, Fin.is_lt]
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ ∑ x : Fin pb.dim, ↑(Finset.card (Ioi x)) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
simp_rw [Fin.card_Ioi, Nat.sub_sub, add_comm 1]
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ ∑ x : Fin pb.dim, ↑(pb.dim - (↑x + 1)) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
simp only [Nat.cast_sub, this, Finset.card_fin, nsmul_eq_mul, sum_const, sum_sub_distrib, Nat.cast_add, Nat.cast_one,
  sum_add_distrib, mul_one]
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ ↑pb.dim * ↑pb.dim - (∑ x : Fin pb.dim, ↑↑x + ↑pb.dim) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
rw [← Nat.cast_sum, ← @Finset.sum_range ℕ _ pb.dim fun i => i, sum_range_id]
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
have hn : n = pb.dim := by
  rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
  exact card_congr (Equiv.symm e)
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ n = pb.dim
[PROOFSTEP]
rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)
[PROOFSTEP]
exact card_congr (Equiv.symm e)
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := even_iff_two_dvd.1 (Nat.even_mul_self_pred _)
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
⊢ ↑2 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
have hle : 1 ≤ pb.dim :=
  by
  rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, FiniteDimensional.finrank_pos_iff]
  infer_instance
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
⊢ 1 ≤ pb.dim
[PROOFSTEP]
rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, FiniteDimensional.finrank_pos_iff]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
⊢ Nontrivial L
[PROOFSTEP]
infer_instance
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
hle : 1 ≤ pb.dim
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
[PROOFSTEP]
rw [hn, Nat.cast_div h₂ hne, Nat.cast_mul, Nat.cast_sub hle]
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
hle : 1 ≤ pb.dim
⊢ ↑pb.dim * ↑pb.dim - (↑pb.dim * (↑pb.dim - ↑1) / ↑2 + ↑pb.dim) = ↑pb.dim * (↑pb.dim - ↑1) / ↑2
[PROOFSTEP]
field_simp
[GOAL]
case e_a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
hle : 1 ≤ pb.dim
⊢ ↑pb.dim * ↑pb.dim * 2 - (↑pb.dim * (↑pb.dim - 1) + ↑pb.dim * 2) = ↑pb.dim * (↑pb.dim - 1)
[PROOFSTEP]
ring
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
⊢ discr K ↑pb.basis = (-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
let E := AlgebraicClosure L
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
⊢ discr K ↑pb.basis = (-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
letI := fun a b : E => Classical.propDecidable (Eq a b)
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
⊢ discr K ↑pb.basis = (-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
have e : Fin pb.dim ≃ (L →ₐ[K] E) := by
  refine' equivOfCardEq _
  rw [Fintype.card_fin, AlgHom.card]
  exact (PowerBasis.finrank pb).symm
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
⊢ Fin pb.dim ≃ (L →ₐ[K] E)
[PROOFSTEP]
refine' equivOfCardEq _
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
⊢ Fintype.card (Fin pb.dim) = Fintype.card (L →ₐ[K] E)
[PROOFSTEP]
rw [Fintype.card_fin, AlgHom.card]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
⊢ pb.dim = n
[PROOFSTEP]
exact (PowerBasis.finrank pb).symm
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ discr K ↑pb.basis = (-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
have hnodup : ((minpoly K pb.gen).map (algebraMap K E)).roots.Nodup :=
  nodup_roots (Separable.map (IsSeparable.separable K pb.gen))
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
⊢ discr K ↑pb.basis = (-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ ((minpoly K pb.gen).map (algebraMap K E)).roots :=
  by
  intro σ
  rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply]
  repeat' simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
⊢ ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
[PROOFSTEP]
intro σ
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
σ : L →ₐ[K] E
⊢ ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
[PROOFSTEP]
rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_algHom_apply]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
σ : L →ₐ[K] E
⊢ ↑σ (↑(aeval pb.gen) (minpoly K pb.gen)) = 0
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
[PROOFSTEP]
repeat' simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
σ : L →ₐ[K] E
⊢ ↑σ (↑(aeval pb.gen) (minpoly K pb.gen)) = 0
[PROOFSTEP]
simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
[PROOFSTEP]
simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ discr K ↑pb.basis = (-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
apply (algebraMap K E).injective
[GOAL]
case a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ ↑(algebraMap K E) (discr K ↑pb.basis) =
    ↑(algebraMap K E) ((-1) ^ (n * (n - 1) / 2) * ↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen))))
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_pow, RingHom.map_neg, RingHom.map_one, discr_powerBasis_eq_prod'' _ _ _ e]
[GOAL]
case a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ (-1) ^ (n * (n - 1) / 2) *
      ∏ i : Fin pb.dim, ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen) =
    (-1) ^ (n * (n - 1) / 2) * ↑(algebraMap K E) (↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen))))
[PROOFSTEP]
congr
[GOAL]
case a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ ∏ i : Fin pb.dim, ∏ j in Ioi i, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) * (↑(↑e i) pb.gen - ↑(↑e j) pb.gen) =
    ↑(algebraMap K E) (↑(norm K) (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen))))
[PROOFSTEP]
rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag]
[GOAL]
case a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ ∏ i : Fin pb.dim, ∏ j in {i}ᶜ, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) =
    ∏ σ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E, ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
conv_rhs =>
  congr
  rfl
  ext σ
  rw [← aeval_algHom_apply,
    aeval_root_derivative_of_splits (minpoly.monic (IsSeparable.isIntegral K pb.gen)) (IsAlgClosed.splits_codomain _)
      (hroots σ),
    ← Finset.prod_mk _ (hnodup.erase _)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
| ∏ σ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E, ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
  congr
  rfl
  ext σ
  rw [← aeval_algHom_apply,
    aeval_root_derivative_of_splits (minpoly.monic (IsSeparable.isIntegral K pb.gen)) (IsAlgClosed.splits_codomain _)
      (hroots σ),
    ← Finset.prod_mk _ (hnodup.erase _)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
| ∏ σ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E, ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
  congr
  rfl
  ext σ
  rw [← aeval_algHom_apply,
    aeval_root_derivative_of_splits (minpoly.monic (IsSeparable.isIntegral K pb.gen)) (IsAlgClosed.splits_codomain _)
      (hroots σ),
    ← Finset.prod_mk _ (hnodup.erase _)]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
| ∏ σ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E, ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
congr
[GOAL]
case s
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
| univ
case f
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
| fun σ => ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
rfl
[GOAL]
case f
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
| fun σ => ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
ext σ
[GOAL]
case f.h
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E
| ↑σ (↑(aeval pb.gen) (↑derivative (minpoly K pb.gen)))
[PROOFSTEP]
rw [← aeval_algHom_apply,
  aeval_root_derivative_of_splits (minpoly.monic (IsSeparable.isIntegral K pb.gen)) (IsAlgClosed.splits_codomain _)
    (hroots σ),
  ← Finset.prod_mk _ (hnodup.erase _)]
[GOAL]
case a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ ∏ i : Fin pb.dim, ∏ j in {i}ᶜ, (↑(↑e j) pb.gen - ↑(↑e i) pb.gen) =
    ∏ σ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E,
      ∏ a in
        { val := Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen),
          nodup :=
            (_ :
              Multiset.Nodup
                (Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen))) },
        (↑σ pb.gen - a)
[PROOFSTEP]
rw [prod_sigma', prod_sigma']
[GOAL]
case a.e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
⊢ ∏ x in Finset.sigma univ fun i => {i}ᶜ, (↑(↑e x.snd) pb.gen - ↑(↑e x.fst) pb.gen) =
    ∏ x in
      Finset.sigma univ fun σ =>
        { val := Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen),
          nodup :=
            (_ :
              Multiset.Nodup
                (Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen))) },
      (↑x.fst pb.gen - x.snd)
[PROOFSTEP]
refine'
  prod_bij (fun i _ => ⟨e i.2, e i.1 pb.gen⟩) (fun i hi => _) (fun i _ => by simp) (fun i j hi hj hij => _) fun σ hσ =>
    _
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
x✝ : i ∈ Finset.sigma univ fun i => {i}ᶜ
⊢ ↑(↑e i.snd) pb.gen - ↑(↑e i.fst) pb.gen =
    ↑((fun i x => { fst := ↑e i.snd, snd := ↑(↑e i.fst) pb.gen }) i x✝).fst pb.gen -
      ((fun i x => { fst := ↑e i.snd, snd := ↑(↑e i.fst) pb.gen }) i x✝).snd
[PROOFSTEP]
simp
[GOAL]
case a.e_a.refine'_1
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
⊢ (fun i x => { fst := ↑e i.snd, snd := ↑(↑e i.fst) pb.gen }) i hi ∈
    Finset.sigma univ fun σ =>
      { val := Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen),
        nodup :=
          (_ :
            Multiset.Nodup (Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen))) }
[PROOFSTEP]
simp only [true_and_iff, Finset.mem_mk, mem_univ, mem_sigma]
[GOAL]
case a.e_a.refine'_1
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
⊢ ↑(↑e i.fst) pb.gen ∈
    Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑(↑e i.snd) pb.gen)
[PROOFSTEP]
rw [Multiset.mem_erase_of_ne fun h => ?_]
[GOAL]
case a.e_a.refine'_1
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
⊢ ↑(↑e i.fst) pb.gen ∈ roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))
[PROOFSTEP]
exact
  hroots
    _
      -- Porting note: `@mem_compl` was not necessary.
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
h : ↑(↑e i.fst) pb.gen = ↑(↑e i.snd) pb.gen
⊢ False
[PROOFSTEP]
simp only [true_and_iff, mem_univ, Ne.def, mem_sigma, @mem_compl _ _ _ (_), mem_singleton] at hi
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
h : ↑(↑e i.fst) pb.gen = ↑(↑e i.snd) pb.gen
hi : ¬i.snd = i.fst
⊢ False
[PROOFSTEP]
rw [← PowerBasis.liftEquiv_apply_coe, ← PowerBasis.liftEquiv_apply_coe] at h
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i : (_ : Fin pb.dim) × Fin pb.dim
h : ↑(↑(PowerBasis.liftEquiv pb) (↑e i.fst)) = ↑(↑(PowerBasis.liftEquiv pb) (↑e i.snd))
hi : ¬i.snd = i.fst
⊢ False
[PROOFSTEP]
exact hi (e.injective <| pb.liftEquiv.injective <| Subtype.eq h.symm)
[GOAL]
case a.e_a.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i j : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
hj : j ∈ Finset.sigma univ fun i => {i}ᶜ
hij :
  (fun i x => { fst := ↑e i.snd, snd := ↑(↑e i.fst) pb.gen }) i hi =
    (fun i x => { fst := ↑e i.snd, snd := ↑(↑e i.fst) pb.gen }) j hj
⊢ i = j
[PROOFSTEP]
simp only [Sigma.mk.inj_iff, EmbeddingLike.apply_eq_iff_eq, heq_eq_eq] at hij
[GOAL]
case a.e_a.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i j : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
hj : j ∈ Finset.sigma univ fun i => {i}ᶜ
hij : i.snd = j.snd ∧ ↑(↑e i.fst) pb.gen = ↑(↑e j.fst) pb.gen
⊢ i = j
[PROOFSTEP]
have h := hij.2
[GOAL]
case a.e_a.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i j : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
hj : j ∈ Finset.sigma univ fun i => {i}ᶜ
hij : i.snd = j.snd ∧ ↑(↑e i.fst) pb.gen = ↑(↑e j.fst) pb.gen
h : ↑(↑e i.fst) pb.gen = ↑(↑e j.fst) pb.gen
⊢ i = j
[PROOFSTEP]
rw [← PowerBasis.liftEquiv_apply_coe, ← PowerBasis.liftEquiv_apply_coe] at h
[GOAL]
case a.e_a.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i j : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
hj : j ∈ Finset.sigma univ fun i => {i}ᶜ
hij : i.snd = j.snd ∧ ↑(↑e i.fst) pb.gen = ↑(↑e j.fst) pb.gen
h : ↑(↑(PowerBasis.liftEquiv pb) (↑e i.fst)) = ↑(↑(PowerBasis.liftEquiv pb) (↑e j.fst))
⊢ i = j
[PROOFSTEP]
refine' Sigma.eq (Equiv.injective e (Equiv.injective _ (Subtype.eq h))) (by simp [hij.1])
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
i j : (_ : Fin pb.dim) × Fin pb.dim
hi : i ∈ Finset.sigma univ fun i => {i}ᶜ
hj : j ∈ Finset.sigma univ fun i => {i}ᶜ
hij : i.snd = j.snd ∧ ↑(↑e i.fst) pb.gen = ↑(↑e j.fst) pb.gen
h : ↑(↑(PowerBasis.liftEquiv pb) (↑e i.fst)) = ↑(↑(PowerBasis.liftEquiv pb) (↑e j.fst))
⊢ Eq.recOn (_ : i.fst = j.fst) i.snd = j.snd
[PROOFSTEP]
simp [hij.1]
[GOAL]
case a.e_a.refine'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ ∈
    Finset.sigma univ fun σ =>
      { val := Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen),
        nodup :=
          (_ :
            Multiset.Nodup (Multiset.erase (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))) (↑σ pb.gen))) }
⊢ ∃ a ha, σ = (fun i x => { fst := ↑e i.snd, snd := ↑(↑e i.fst) pb.gen }) a ha
[PROOFSTEP]
simp only [true_and_iff, Finset.mem_mk, mem_univ, mem_sigma] at hσ ⊢
[GOAL]
case a.e_a.refine'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ ∃ a h, σ = { fst := ↑e a.snd, snd := ↑(↑e a.fst) pb.gen }
[PROOFSTEP]
simp only [Sigma.exists, exists_prop, mem_compl, mem_singleton, Ne.def]
[GOAL]
case a.e_a.refine'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ ∃ a b, b ∈ {a}ᶜ ∧ σ = { fst := ↑e b, snd := ↑(↑e a) pb.gen }
[PROOFSTEP]
refine' ⟨e.symm (PowerBasis.lift pb σ.2 _), e.symm σ.1, ⟨_, Sigma.eq _ _⟩⟩
[GOAL]
case a.e_a.refine'_3.refine'_1
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ ↑(aeval σ.snd) (minpoly K pb.gen) = 0
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def, ← mem_roots]
[GOAL]
case a.e_a.refine'_3.refine'_1
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ σ.snd ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
[PROOFSTEP]
exact Multiset.erase_subset _ _ hσ
[GOAL]
case a.e_a.refine'_3.refine'_1
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
[PROOFSTEP]
simp [minpoly.ne_zero (IsSeparable.isIntegral K pb.gen)]
  -- Porting note: the `simp only` was not needed.
[GOAL]
case a.e_a.refine'_3.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ ↑e.symm σ.fst ∈ {↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0))}ᶜ
[PROOFSTEP]
simp only [@mem_compl _ _ _ (_), mem_singleton]
[GOAL]
case a.e_a.refine'_3.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ ¬↑e.symm σ.fst = ↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0))
[PROOFSTEP]
intro h
[GOAL]
case a.e_a.refine'_3.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
h : ↑e.symm σ.fst = ↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0))
⊢ False
[PROOFSTEP]
replace h := AlgHom.congr_fun (Equiv.injective _ h) pb.gen
[GOAL]
case a.e_a.refine'_3.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
h : ↑σ.fst pb.gen = ↑(PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0)) pb.gen
⊢ False
[PROOFSTEP]
rw [PowerBasis.lift_gen] at h
[GOAL]
case a.e_a.refine'_3.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
h : ↑σ.fst pb.gen = σ.snd
⊢ False
[PROOFSTEP]
rw [← h] at hσ
[GOAL]
case a.e_a.refine'_3.refine'_2
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  ↑σ.fst pb.gen ∈
    Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
h : ↑σ.fst pb.gen = σ.snd
⊢ False
[PROOFSTEP]
exact hnodup.not_mem_erase hσ
[GOAL]
case a.e_a.refine'_3.refine'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ σ.fst =
    { fst := ↑e (↑e.symm σ.fst),
        snd := ↑(↑e (↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0)))) pb.gen }.fst
case a.e_a.refine'_3.refine'_4
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ Eq.recOn ?a.e_a.refine'_3.refine'_3✝ σ.snd =
    { fst := ↑e (↑e.symm σ.fst),
        snd := ↑(↑e (↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0)))) pb.gen }.snd
[PROOFSTEP]
all_goals simp
[GOAL]
case a.e_a.refine'_3.refine'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ σ.fst =
    { fst := ↑e (↑e.symm σ.fst),
        snd := ↑(↑e (↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0)))) pb.gen }.fst
[PROOFSTEP]
simp
[GOAL]
case a.e_a.refine'_3.refine'_4
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁶ : DecidableEq ι
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A C
ι' : Type u_1
inst✝¹⁰ : Fintype ι'
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι'
K : Type u
L : Type v
E✝ : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E✝
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E✝
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E✝
b : ι → L
pb : PowerBasis K L
inst✝ : IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : Multiset.Nodup (roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
hroots : ∀ (σ : L →ₐ[K] E), ↑σ pb.gen ∈ roots (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
σ : (_ : (fun x => L) (↑derivative (minpoly K pb.gen)) →ₐ[K] E) × E
hσ :
  σ.snd ∈ Multiset.erase (roots (Polynomial.map (algebraMap K (AlgebraicClosure L)) (minpoly K pb.gen))) (↑σ.fst pb.gen)
⊢ Eq.recOn (_ : σ.fst = ↑e (↑e.symm σ.fst)) σ.snd =
    { fst := ↑e (↑e.symm σ.fst),
        snd := ↑(↑e (↑e.symm (PowerBasis.lift pb σ.snd (_ : ↑(aeval σ.snd) (minpoly K pb.gen) = 0)))) pb.gen }.snd
[PROOFSTEP]
simp
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁹ : DecidableEq ι
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : CommRing C
inst✝¹⁴ : Algebra A C
ι' : Type u_1
inst✝¹³ : Fintype ι'
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Field E
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra K E
inst✝⁵ : Module.Finite K L
inst✝⁴ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)
[PROOFSTEP]
classical
rw [discr_def]
exact IsIntegral.det fun i j => isIntegral_trace (isIntegral_mul (h i) (h j))
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁹ : DecidableEq ι
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : CommRing C
inst✝¹⁴ : Algebra A C
ι' : Type u_1
inst✝¹³ : Fintype ι'
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Field E
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra K E
inst✝⁵ : Module.Finite K L
inst✝⁴ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)
[PROOFSTEP]
rw [discr_def]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝¹⁹ : DecidableEq ι
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : CommRing C
inst✝¹⁴ : Algebra A C
ι' : Type u_1
inst✝¹³ : Fintype ι'
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Field E
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra K E
inst✝⁵ : Module.Finite K L
inst✝⁴ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (det (traceMatrix K b))
[PROOFSTEP]
exact IsIntegral.det fun i j => isIntegral_trace (isIntegral_mul (h i) (h j))
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (Basis.toMatrix b' (↑b) i j)
⊢ discr ℚ ↑b = discr ℚ ↑b'
[PROOFSTEP]
replace h' : ∀ i j, IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b')) i j)
[GOAL]
case h'
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (Basis.toMatrix b' (↑b) i j)
⊢ ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
[PROOFSTEP]
intro i j
[GOAL]
case h'
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (Basis.toMatrix b' (↑b) i j)
i j : ι'
⊢ IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
[PROOFSTEP]
convert
  h' i
    ((b.indexEquiv b').symm j)
      -- Porting note: `simp; rfl` was `simpa`.
[GOAL]
case h.e'_6
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (Basis.toMatrix b' (↑b) i j)
i j : ι'
⊢ Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j =
    Basis.toMatrix b' (↑b) i (↑(Basis.indexEquiv b b').symm j)
[PROOFSTEP]
simp
[GOAL]
case h.e'_6
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (Basis.toMatrix b' (↑b) i j)
i j : ι'
⊢ Basis.toMatrix b' (↑b ∘ ↑(Basis.indexEquiv b b').symm) i j =
    Basis.toMatrix b' (↑b) i (↑(Basis.indexEquiv b b').symm j)
[PROOFSTEP]
rfl
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
⊢ discr ℚ ↑b = discr ℚ ↑b'
[PROOFSTEP]
classical
rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul, ← one_mul (discr ℚ b),
  Basis.coe_reindex, discr_reindex]
congr
have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det := IsIntegral.det fun i j => h _ _
obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
have hunit : IsUnit r :=
  by
  have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det := IsIntegral.det fun i j => h' _ _
  obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
  refine' isUnit_iff_exists_inv.2 ⟨r', _⟩
  suffices algebraMap ℤ ℚ (r * r') = 1
    by
    rw [← RingHom.map_one (algebraMap ℤ ℚ)] at this
    exact (IsFractionRing.injective ℤ ℚ) this
  rw [RingHom.map_mul, hr, hr', ← det_mul, Basis.toMatrix_mul_toMatrix_flip, det_one]
rw [← RingHom.map_one (algebraMap ℤ ℚ), ← hr]
cases' Int.isUnit_iff.1 hunit with hp hm
· simp [hp]
· simp [hm]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
⊢ discr ℚ ↑b = discr ℚ ↑b'
[PROOFSTEP]
rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul, ← one_mul (discr ℚ b),
  Basis.coe_reindex, discr_reindex]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
⊢ 1 * discr ℚ ↑b = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b') ^ 2 * discr ℚ ↑b
[PROOFSTEP]
congr
[GOAL]
case e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
⊢ 1 = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b') ^ 2
[PROOFSTEP]
have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det := IsIntegral.det fun i j => h _ _
[GOAL]
case e_a
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
⊢ 1 = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b') ^ 2
[PROOFSTEP]
obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
[GOAL]
case e_a.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
⊢ 1 = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b') ^ 2
[PROOFSTEP]
have hunit : IsUnit r :=
  by
  have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det := IsIntegral.det fun i j => h' _ _
  obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
  refine' isUnit_iff_exists_inv.2 ⟨r', _⟩
  suffices algebraMap ℤ ℚ (r * r') = 1
    by
    rw [← RingHom.map_one (algebraMap ℤ ℚ)] at this
    exact (IsFractionRing.injective ℤ ℚ) this
  rw [RingHom.map_mul, hr, hr', ← det_mul, Basis.toMatrix_mul_toMatrix_flip, det_one]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
⊢ IsUnit r
[PROOFSTEP]
have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det := IsIntegral.det fun i j => h' _ _
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
this : IsIntegral ℤ (det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b'))))
⊢ IsUnit r
[PROOFSTEP]
obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
[GOAL]
case intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
this : IsIntegral ℤ (det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b'))))
r' : ℤ
hr' : ↑(algebraMap ℤ ℚ) r' = det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b')))
⊢ IsUnit r
[PROOFSTEP]
refine' isUnit_iff_exists_inv.2 ⟨r', _⟩
[GOAL]
case intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
this : IsIntegral ℤ (det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b'))))
r' : ℤ
hr' : ↑(algebraMap ℤ ℚ) r' = det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b')))
⊢ r * r' = 1
[PROOFSTEP]
suffices algebraMap ℤ ℚ (r * r') = 1
  by
  rw [← RingHom.map_one (algebraMap ℤ ℚ)] at this
  exact (IsFractionRing.injective ℤ ℚ) this
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
this✝ : IsIntegral ℤ (det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b'))))
r' : ℤ
hr' : ↑(algebraMap ℤ ℚ) r' = det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b')))
this : ↑(algebraMap ℤ ℚ) (r * r') = 1
⊢ r * r' = 1
[PROOFSTEP]
rw [← RingHom.map_one (algebraMap ℤ ℚ)] at this
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
this✝ : IsIntegral ℤ (det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b'))))
r' : ℤ
hr' : ↑(algebraMap ℤ ℚ) r' = det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b')))
this : ↑(algebraMap ℤ ℚ) (r * r') = ↑(algebraMap ℤ ℚ) 1
⊢ r * r' = 1
[PROOFSTEP]
exact (IsFractionRing.injective ℤ ℚ) this
[GOAL]
case intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
this : IsIntegral ℤ (det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b'))))
r' : ℤ
hr' : ↑(algebraMap ℤ ℚ) r' = det (Basis.toMatrix b' ↑(Basis.reindex b (Basis.indexEquiv b b')))
⊢ ↑(algebraMap ℤ ℚ) (r * r') = 1
[PROOFSTEP]
rw [RingHom.map_mul, hr, hr', ← det_mul, Basis.toMatrix_mul_toMatrix_flip, det_one]
[GOAL]
case e_a.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
hunit : IsUnit r
⊢ 1 = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b') ^ 2
[PROOFSTEP]
rw [← RingHom.map_one (algebraMap ℤ ℚ), ← hr]
[GOAL]
case e_a.intro
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
hunit : IsUnit r
⊢ ↑(algebraMap ℤ ℚ) 1 = ↑(algebraMap ℤ ℚ) r ^ 2
[PROOFSTEP]
cases' Int.isUnit_iff.1 hunit with hp hm
[GOAL]
case e_a.intro.inl
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
hunit : IsUnit r
hp : r = 1
⊢ ↑(algebraMap ℤ ℚ) 1 = ↑(algebraMap ℤ ℚ) r ^ 2
[PROOFSTEP]
simp [hp]
[GOAL]
case e_a.intro.inr
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝²⁰ : DecidableEq ι
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : CommRing C
inst✝¹⁵ : Algebra A C
ι' : Type u_1
inst✝¹⁴ : Fintype ι'
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field E
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K E
inst✝⁶ : Module.Finite K L
inst✝⁵ : IsAlgClosed E
b✝ : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁴ : CommRing R
inst✝³ : Algebra R K
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R K L
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (↑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (Basis.toMatrix b' (↑(Basis.reindex b (Basis.indexEquiv b b'))) i j)
hint : IsIntegral ℤ (det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b'))
r : ℤ
hr : ↑(algebraMap ℤ ℚ) r = det (Basis.toMatrix (Basis.reindex b (Basis.indexEquiv b b')) ↑b')
hunit : IsUnit r
hm : r = -1
⊢ ↑(algebraMap ℤ ℚ) 1 = ↑(algebraMap ℤ ℚ) r ^ 2
[PROOFSTEP]
simp [hm]
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ discr K ↑B.basis • z ∈ adjoin R {B.gen}
[PROOFSTEP]
have hinv : IsUnit (traceMatrix K B.basis).det := by simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ IsUnit (det (traceMatrix K ↑B.basis))
[PROOFSTEP]
simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
⊢ discr K ↑B.basis • z ∈ adjoin R {B.gen}
[PROOFSTEP]
have H :
  (traceMatrix K B.basis).det • (traceMatrix K B.basis).mulVec (B.basis.equivFun z) =
    (traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) :=
  by congr; exact traceMatrix_of_basis_mulVec _ _
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
⊢ det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
[PROOFSTEP]
congr
[GOAL]
case e_a
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
⊢ mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) = fun i => ↑(trace K L) (z * ↑B.basis i)
[PROOFSTEP]
exact traceMatrix_of_basis_mulVec _ _
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
⊢ discr K ↑B.basis • z ∈ adjoin R {B.gen}
[PROOFSTEP]
have cramer := mulVec_cramer (traceMatrix K B.basis) fun i => trace K L (z * B.basis i)
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
⊢ discr K ↑B.basis • z ∈ adjoin R {B.gen}
[PROOFSTEP]
suffices ∀ i, ((traceMatrix K B.basis).det • B.basis.equivFun z) i ∈ (⊥ : Subalgebra R K)
  by
  rw [← B.basis.sum_repr z, Finset.smul_sum]
  refine' Subalgebra.sum_mem _ fun i _ => _
  replace this := this i
  rw [← discr_def, Pi.smul_apply, mem_bot] at this
  obtain ⟨r, hr⟩ := this
  rw [Basis.equivFun_apply] at hr
  rw [← smul_assoc, ← hr, algebraMap_smul]
  refine' Subalgebra.smul_mem _ _ _
  rw [B.basis_eq_pow i]
  refine' Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
this : ∀ (i : Fin B.dim), (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
⊢ discr K ↑B.basis • z ∈ adjoin R {B.gen}
[PROOFSTEP]
rw [← B.basis.sum_repr z, Finset.smul_sum]
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
this : ∀ (i : Fin B.dim), (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
⊢ ∑ x : Fin B.dim, discr K ↑B.basis • ↑(↑B.basis.repr z) x • ↑B.basis x ∈ adjoin R {B.gen}
[PROOFSTEP]
refine' Subalgebra.sum_mem _ fun i _ => _
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
this : ∀ (i : Fin B.dim), (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
i : Fin B.dim
x✝ : i ∈ univ
⊢ discr K ↑B.basis • ↑(↑B.basis.repr z) i • ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
replace this := this i
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
this : (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
⊢ discr K ↑B.basis • ↑(↑B.basis.repr z) i • ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
rw [← discr_def, Pi.smul_apply, mem_bot] at this
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
this : discr K ↑B.basis • ↑(Basis.equivFun B.basis) z i ∈ Set.range ↑(algebraMap R K)
⊢ discr K ↑B.basis • ↑(↑B.basis.repr z) i • ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
obtain ⟨r, hr⟩ := this
[GOAL]
case intro
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : ↑(algebraMap R K) r = discr K ↑B.basis • ↑(Basis.equivFun B.basis) z i
⊢ discr K ↑B.basis • ↑(↑B.basis.repr z) i • ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
rw [Basis.equivFun_apply] at hr
[GOAL]
case intro
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : ↑(algebraMap R K) r = discr K ↑B.basis • ↑(↑B.basis.repr z) i
⊢ discr K ↑B.basis • ↑(↑B.basis.repr z) i • ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
rw [← smul_assoc, ← hr, algebraMap_smul]
[GOAL]
case intro
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : ↑(algebraMap R K) r = discr K ↑B.basis • ↑(↑B.basis.repr z) i
⊢ r • ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
refine' Subalgebra.smul_mem _ _ _
[GOAL]
case intro
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : ↑(algebraMap R K) r = discr K ↑B.basis • ↑(↑B.basis.repr z) i
⊢ ↑B.basis i ∈ adjoin R {B.gen}
[PROOFSTEP]
rw [B.basis_eq_pow i]
[GOAL]
case intro
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : ↑(algebraMap R K) r = discr K ↑B.basis • ↑(↑B.basis.repr z) i
⊢ B.gen ^ ↑i ∈ adjoin R {B.gen}
[PROOFSTEP]
refine' Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
⊢ ∀ (i : Fin B.dim), (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
[PROOFSTEP]
intro i
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
⊢ (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
[PROOFSTEP]
rw [← H, ← mulVec_smul] at cramer
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
cramer :
  mulVec (traceMatrix K ↑B.basis) (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    mulVec (traceMatrix K ↑B.basis) (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z)
i : Fin B.dim
⊢ (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
[PROOFSTEP]
replace cramer := congr_arg (mulVec (traceMatrix K B.basis)⁻¹) cramer
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  mulVec (traceMatrix K ↑B.basis)⁻¹
      (mulVec (traceMatrix K ↑B.basis)
        (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i))) =
    mulVec (traceMatrix K ↑B.basis)⁻¹
      (mulVec (traceMatrix K ↑B.basis) (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z))
⊢ (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
[PROOFSTEP]
rw [mulVec_mulVec, nonsing_inv_mul _ hinv, mulVec_mulVec, nonsing_inv_mul _ hinv, one_mulVec, one_mulVec] at cramer
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
⊢ (det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z) i ∈ ⊥
[PROOFSTEP]
rw [← congr_fun cramer i, cramer_apply, det_apply]
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
⊢ ∑ σ : Equiv.Perm (Fin B.dim),
      ↑Equiv.Perm.sign σ •
        ∏ i_1 : Fin B.dim,
          updateColumn (traceMatrix K ↑B.basis) i (fun i => ↑(trace K L) (z * ↑B.basis i)) (↑σ i_1) i_1 ∈
    ⊥
[PROOFSTEP]
refine' Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => _) _
[GOAL]
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
⊢ updateColumn (traceMatrix K ↑B.basis) i (fun i => ↑(trace K L) (z * ↑B.basis i)) (↑σ j) j ∈ ⊥
[PROOFSTEP]
by_cases hji : j = i
[GOAL]
case pos
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : j = i
⊢ updateColumn (traceMatrix K ↑B.basis) i (fun i => ↑(trace K L) (z * ↑B.basis i)) (↑σ j) j ∈ ⊥
[PROOFSTEP]
simp only [updateColumn_apply, hji, eq_self_iff_true, PowerBasis.coe_basis]
[GOAL]
case pos
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : j = i
⊢ (if True then ↑(trace K L) (z * B.gen ^ ↑(↑σ i)) else traceMatrix K (fun i => B.gen ^ ↑i) (↑σ i) i) ∈ ⊥
[PROOFSTEP]
exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| isIntegral_mul hz <| IsIntegral.pow hint _)
[GOAL]
case neg
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ updateColumn (traceMatrix K ↑B.basis) i (fun i => ↑(trace K L) (z * ↑B.basis i)) (↑σ j) j ∈ ⊥
[PROOFSTEP]
simp only [updateColumn_apply, hji, PowerBasis.coe_basis]
[GOAL]
case neg
A : Type u
B✝ : Type v
C : Type z
ι : Type w
inst✝²³ : DecidableEq ι
inst✝²² : CommRing A
inst✝²¹ : CommRing B✝
inst✝²⁰ : Algebra A B✝
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A C
ι' : Type u_1
inst✝¹⁷ : Fintype ι'
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : DecidableEq ι'
K : Type u
L : Type v
E : Type z
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Field E
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra K E
inst✝⁹ : Module.Finite K L
inst✝⁸ : IsAlgClosed E
b : ι → L
pb : PowerBasis K L
R : Type z
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsDomain R
inst✝² : IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det (traceMatrix K ↑B.basis))
H :
  det (traceMatrix K ↑B.basis) • mulVec (traceMatrix K ↑B.basis) (↑(Basis.equivFun B.basis) z) =
    det (traceMatrix K ↑B.basis) • fun i => ↑(trace K L) (z * ↑B.basis i)
i : Fin B.dim
cramer :
  (↑(Matrix.cramer (traceMatrix K ↑B.basis)) fun i => ↑(trace K L) (z * ↑B.basis i)) =
    det (traceMatrix K ↑B.basis) • ↑(Basis.equivFun B.basis) z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (if False then ↑(trace K L) (z * B.gen ^ ↑(↑σ j)) else traceMatrix K (fun i => B.gen ^ ↑i) (↑σ j) j) ∈ ⊥
[PROOFSTEP]
exact
  mem_bot.2
    (IsIntegrallyClosed.isIntegral_iff.1 <|
      isIntegral_trace <| isIntegral_mul (IsIntegral.pow hint _) (IsIntegral.pow hint _))
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ↑b = discr ℤ ↑b'
[PROOFSTEP]
convert Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)
[GOAL]
case h.e'_2.h.e'_9
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ ↑b = vecMul (↑b') (Matrix.map (Basis.toMatrix b' ↑b) ↑(algebraMap ℤ A))
[PROOFSTEP]
rw [Basis.toMatrix_map_vecMul]
[GOAL]
case h.e'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ↑b' = det (Basis.toMatrix b' ↑b) ^ 2 * discr ℤ ↑b'
[PROOFSTEP]
suffices IsUnit (b'.toMatrix b).det by
  rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
  rw [this, one_mul]
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : IsUnit (det (Basis.toMatrix b' ↑b))
⊢ discr ℤ ↑b' = det (Basis.toMatrix b' ↑b) ^ 2 * discr ℤ ↑b'
[PROOFSTEP]
rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
[GOAL]
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : det (Basis.toMatrix b' ↑b) ^ 2 = 1
⊢ discr ℤ ↑b' = det (Basis.toMatrix b' ↑b) ^ 2 * discr ℤ ↑b'
[PROOFSTEP]
rw [this, one_mul]
[GOAL]
case h.e'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (det (Basis.toMatrix b' ↑b))
[PROOFSTEP]
rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']
[GOAL]
case h.e'_3
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra A C
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (det (↑(LinearMap.toMatrix b b') LinearMap.id))
[PROOFSTEP]
exact LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'