n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ P M
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
⊢ P M
let Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
no goals
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
this : Q M
⊢ P M
exact this.2
case hdiag
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ ∀ (D : n → 𝕜), det (diagonal D) = det M → Q (diagonal D)

case htransvec
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ ∀ (t : TransvectionStruct n 𝕜), Q (toMatrix t)

case hmul
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A ⬝ B)
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ Q M
apply diagonal_transvection_induction Q M
case hdiag
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
⊢ Q (diagonal D)
case hdiag
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ ∀ (D : n → 𝕜), det (diagonal D) = det M → Q (diagonal D)
intro D hD
case hdiag
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
detD : det (diagonal D) ≠ 0
⊢ Q (diagonal D)
case hdiag
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
⊢ Q (diagonal D)
have detD : det (diagonal D) ≠ 0 := by
  rw [hD]
  exact hMdet
no goals
case hdiag
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
detD : det (diagonal D) ≠ 0
⊢ Q (diagonal D)
exact ⟨detD, hdiag _ detD⟩
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
⊢ det M ≠ 0
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
⊢ det (diagonal D) ≠ 0
rw [hD]
no goals
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
D : n → 𝕜
hD : det (diagonal D) = det M
⊢ det M ≠ 0
exact hMdet
case htransvec
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
t : TransvectionStruct n 𝕜
⊢ Q (toMatrix t)
case htransvec
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ ∀ (t : TransvectionStruct n 𝕜), Q (toMatrix t)
intro t
no goals
case htransvec
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
t : TransvectionStruct n 𝕜
⊢ Q (toMatrix t)
exact ⟨by simp, htransvec t⟩
no goals
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
t : TransvectionStruct n 𝕜
⊢ det (toMatrix t) ≠ 0
simp
case hmul
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
A B : Matrix n n 𝕜
QA : Q A
QB : Q B
⊢ Q (A ⬝ B)
case hmul
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
⊢ ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A ⬝ B)
intro A B QA QB
no goals
case hmul
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
A B : Matrix n n 𝕜
QA : Q A
QB : Q B
⊢ Q (A ⬝ B)
exact ⟨by simp [QA.1, QB.1], hmul A B QA.1 QB.1 QA.2 QB.2⟩
no goals
n : Type u_1
p : Type ?u.340683
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : det M ≠ 0
hdiag : ∀ (D : n → 𝕜), det (diagonal D) ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), det A ≠ 0 → det B ≠ 0 → P A → P B → P (A ⬝ B)
Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
A B : Matrix n n 𝕜
QA : Q A
QB : Q B
⊢ det (A ⬝ B) ≠ 0
simp [QA.1, QB.1]