awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ Eq.{v + 1} (α := R)
    (∏ i : n, A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i)
    (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) i) i)
have h : ∀ (x : n),
  A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) x : n) x =
    A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) ((e : (a : n) → m) x : m))
      ((e : (a : n) → m) x)
Tactic: apply Fintype.prod_equiv e
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
i : n
⊢ A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) ((e : (a : n) → m) i : m))
      ((e : (a : n) → m) i)
have h : A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
  A ((e : (a : n) → m) ((σ : (a : n) → n) ((e.symm : (a : m) → n) ((e : (a : n) → m) i : m) : n) : n))
    ((e : (a : n) → m) i)
Tactic: rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
i : n
h :
  A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((e : (a : n) → m) ((σ : (a : n) → n) ((e.symm : (a : m) → n) ((e : (a : n) → m) i : m) : n) : n))
      ((e : (a : n) → m) i)
⊢ A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) ((e : (a : n) → m) i : m))
      ((e : (a : n) → m) i)
have h₁ : A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
  A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i)
Tactic: rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
i : n
h :
  A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((e : (a : n) → m) ((σ : (a : n) → n) ((e.symm : (a : m) → n) ((e : (a : n) → m) i : m) : n) : n))
      ((e : (a : n) → m) i)
h₁ :
  A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i)
⊢ A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) ((e : (a : n) → m) i : m))
      ((e : (a : n) → m) i)
have h₂ : A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i) =
  A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i)
Tactic: rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ e₂ = e₁.trans (e₁.symm.trans e₂)
have H : ∀ (x : n), Eq.{u_1 + 1} (α := m) ((e₂ : (a : n) → m) x : m) ((e₁.trans (e₁.symm.trans e₂) : (a : n) → m) x : m)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))| = |A.det|
have hee : e₂ = e₁.trans (e₁.symm.trans e₂)
Tactic: have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))| = |A.det|
have rw : |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑(e₁.trans (e₁.symm.trans e₂)) : (a : n) → m))| = |A.det|
Tactic: rw [hee]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑(e₁.trans (e₁.symm.trans e₂)) : (a : n) → m))| = |A.det|
have change : |det.{u_3, u_2} (n := n)
      (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
        (⇑e₁ : (a : n) → m))| =
  |A.det|
Tactic: change |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|
have rw : |det (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m))| = |A.det|
Tactic: rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
rw : |det (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m))| = |A.det|
⊢ |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|
have rw₁ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R) * A.det| = |A.det|
Tactic: rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
rw : |det (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m))| = |A.det|
rw₁ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R) * A.det| = |A.det|
⊢ |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|
have rw₂ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R)| * |A.det| = |A.det|
Tactic: rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
rw : |det (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m))| = |A.det|
rw₁ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R) * A.det| = |A.det|
rw₂ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R)| * |A.det| = |A.det|
⊢ |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|
have rw₃ : 1 * |A.det| = |A.det|
Tactic: rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
rw : |det (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m))| = |A.det|
rw₁ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R) * A.det| = |A.det|
rw₂ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R)| * |A.det| = |A.det|
rw₃ : 1 * |A.det| = |A.det|
⊢ |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|
have rw₄ : |A.det| = |A.det|
Tactic: rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M) =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
have trans : Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M))
  (det.{v, u_2} (n := n)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
      ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)))
Tactic: trans ((M.reindex (e.trans e'.symm) (.refl _)).reindex e' e').det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
trans :
  Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M))
    (det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)))
⊢ det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M) =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
have trans₁ : det.{v, u_2} (n := n)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
      ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)) =
  (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
Tactic: trans ((M.reindex (e.trans e'.symm) (.refl _)).reindex e' e').det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M))
    (det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)))
have e_M : Eq (α := Matrix n n R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M : Matrix n n R)
  ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
      ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) :
    Matrix n n R)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ Eq (α := Matrix n n R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M : Matrix n n R)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) :
      Matrix n n R)
have e_M : ∀ (i j : n),
  Eq.{v + 1} (α := R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M i j : R)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) i j :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)) =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
have simp_rw : (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e.trans e'.symm).symm) : ℤ) : R) * M.det =
  (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
Tactic: simp_rw [det_reindex_self, reindex_apply, Equiv.refl_symm, Equiv.coe_refl, det_permute]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
c : R
⊢ (c • A).det = ((diagonal fun (x : n) ↦ c) * A).det
have rw : ((diagonal fun (x : n) ↦ c) * A).det = ((diagonal fun (x : n) ↦ c) * A).det
Tactic: rw [smul_eq_diagonal_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ (c • A).det = c ^ Fintype.card n • A.det
have rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
Tactic: rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
⊢ (c • A).det = c ^ Fintype.card n • A.det
have rw₁ : HSMul.hSMul (β := R) c 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
Tactic: rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
rw₁ : HSMul.hSMul (β := R) c 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
⊢ (c • A).det = c ^ Fintype.card n • A.det
have rw₂ : c ^ Fintype.card n • HPow.hPow (α := R) 1 (Fintype.card n) * A.det = c ^ Fintype.card n • A.det
Tactic: rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
rw₁ : HSMul.hSMul (β := R) c 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
rw₂ : c ^ Fintype.card n • HPow.hPow (α := R) 1 (Fintype.card n) * A.det = c ^ Fintype.card n • A.det
⊢ (c • A).det = c ^ Fintype.card n • A.det
have rw₃ : HSMul.hSMul (β := R) (c ^ Fintype.card n) 1 * A.det = c ^ Fintype.card n • A.det
Tactic: rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
rw₁ : HSMul.hSMul (β := R) c 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
rw₂ : c ^ Fintype.card n • HPow.hPow (α := R) 1 (Fintype.card n) * A.det = c ^ Fintype.card n • A.det
rw₃ : HSMul.hSMul (β := R) (c ^ Fintype.card n) 1 * A.det = c ^ Fintype.card n • A.det
⊢ (c • A).det = c ^ Fintype.card n • A.det
have rw₄ : c ^ Fintype.card n • (1 * A.det) = c ^ Fintype.card n • A.det
Tactic: rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
rw₁ : HSMul.hSMul (β := R) c 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
rw₂ : c ^ Fintype.card n • HPow.hPow (α := R) 1 (Fintype.card n) * A.det = c ^ Fintype.card n • A.det
rw₃ : HSMul.hSMul (β := R) (c ^ Fintype.card n) 1 * A.det = c ^ Fintype.card n • A.det
rw₄ : c ^ Fintype.card n • (1 * A.det) = c ^ Fintype.card n • A.det
⊢ (c • A).det = c ^ Fintype.card n • A.det
have rw₅ : c ^ Fintype.card n • A.det = c ^ Fintype.card n • A.det
Tactic: rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
⊢ (-A).det = HPow.hPow (α := R) (-1) (Fintype.card n) * A.det
have rw : (-A).det = (HSMul.hSMul (α := R) (-1) A).det
Tactic: rw [← det_smul, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
rw : (-A).det = (HSMul.hSMul (α := R) (-1) A).det
⊢ (-A).det = HPow.hPow (α := R) (-1) (Fintype.card n) * A.det
have rw₁ : (-A).det = (-A).det
Tactic: rw [← det_smul, neg_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
⊢ (-A).det = HPow.hPow (α := ℤˣ) (-1) (Fintype.card n) • A.det
have rw : (-A).det = (HSMul.hSMul (α := ℤˣ) (-1) A).det
Tactic: rw [← det_smul_of_tower, Units.neg_smul, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
rw : (-A).det = (HSMul.hSMul (α := ℤˣ) (-1) A).det
⊢ (-A).det = HPow.hPow (α := ℤˣ) (-1) (Fintype.card n) • A.det
have rw₁ : (-A).det = (-HSMul.hSMul (α := ℤˣ) 1 A).det
Tactic: rw [← det_smul_of_tower, Units.neg_smul, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
rw : (-A).det = (HSMul.hSMul (α := ℤˣ) (-1) A).det
rw₁ : (-A).det = (-HSMul.hSMul (α := ℤˣ) 1 A).det
⊢ (-A).det = HPow.hPow (α := ℤˣ) (-1) (Fintype.card n) • A.det
have rw₂ : (-A).det = (-A).det
Tactic: rw [← det_smul_of_tower, Units.neg_smul, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
v : n → R
A : Matrix n n R
⊢ ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ v j * A i j) = A * diagonal v
have a : ∀ (i j : n), (of : (a : n → n → R) → Matrix n n R) (fun (i j : n) ↦ v j * A i j) i j = (A * diagonal v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
v : n → R
A : Matrix n n R
⊢ (A * diagonal v).det = (∏ i : n, v i) * A.det
have rw : A.det * (diagonal v).det = (∏ i : n, v i) * A.det
Tactic: rw [det_mul, det_diagonal, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
v : n → R
A : Matrix n n R
rw : A.det * (diagonal v).det = (∏ i : n, v i) * A.det
⊢ (A * diagonal v).det = (∏ i : n, v i) * A.det
have rw₁ : A.det * ∏ i : n, v i = (∏ i : n, v i) * A.det
Tactic: rw [det_mul, det_diagonal, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
v : n → R
A : Matrix n n R
rw : A.det * (diagonal v).det = (∏ i : n, v i) * A.det
rw₁ : A.det * ∏ i : n, v i = (∏ i : n, v i) * A.det
⊢ (A * diagonal v).det = (∏ i : n, v i) * A.det
have rw₂ : (∏ i : n, v i) * A.det = (∏ i : n, v i) * A.det
Tactic: rw [det_mul, det_diagonal, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ A.det = 0
have rw : Aᵀ.det = 0
Tactic: rw [← det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ M.det = 0
have rw : Mᵀ i = Mᵀ j
Tactic: rw [← det_transpose, det_zero_of_row_eq i_ne_j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det
have rw : (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det
Tactic: rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]