-- Mathlib/NumberTheory/NumberField/EquivReindex.lean
theorem det_of_basisMatrix_non_zero [DecidableEq (K →+* ℂ)] : (basisMatrix K).det ≠ 0

Proof state:
case h.e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑e.symm.symm))

Tactic:
exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
  (fun _ => integralBasis K (e _)) RingHom.equivRatAlgHom).symm

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ (basisMatrix K).det ≠ 0

Tactic:
let e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
⊢ (basisMatrix K).det ≠ 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ basisMatrix K = N

Tactic:
ext:2

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
i✝ j✝ : K →+* ℂ
⊢ basisMatrix K i✝ j✝ = N i✝ j✝

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ (basisMatrix K).det ≠ 0

Tactic:
rw [show (basisMatrix K) = N by
  ext:2; simp only [N, transpose_apply, latticeBasis_apply, integralBasis_apply,
  of_apply, apply_at]; rfl, ← pow_ne_zero_iff two_ne_zero]

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ N.det ^ 2 ≠ 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ N.det ^ 2 ≠ 0

Tactic:
convert (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
  (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))

Result:
case h.e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ ⇑(integralBasis K))

Proof state:
case h.e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ ⇑(integralBasis K))

Tactic:
rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]

Result:
case h.e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑e.symm.symm))

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
i✝ j✝ : K →+* ℂ
⊢ j✝ ((algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) ((equivReindex K) i✝))) =
    Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) (e i)))
      RingHom.equivRatAlgHom i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
⊢ (basisMatrix K).det ≠ 0

Tactic:
let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i))
  RingHom.equivRatAlgHom

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
⊢ (basisMatrix K).det ≠ 0

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
i✝ j✝ : K →+* ℂ
⊢ basisMatrix K i✝ j✝ = N i✝ j✝

Tactic:
simp only [N, transpose_apply, latticeBasis_apply, integralBasis_apply,
of_apply, apply_at]

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom
i✝ j✝ : K →+* ℂ
⊢ j✝ ((algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) ((equivReindex K) i✝))) =
    Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) (e i)))
      RingHom.equivRatAlgHom i✝ j✝