case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsLeftRegular A

case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsRightRegular A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsRegular A
constructor
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => A * x) B = (fun x => A * x) C
⊢ B = C
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsLeftRegular A
intro B C h
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => A * x) B = (fun x => A * x) C
⊢ (fun x => det A • x) B = (fun x => det A • x) C
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => A * x) B = (fun x => A * x) C
⊢ B = C
refine' hA.matrix _
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : A * B = A * C
⊢ det A • B = det A • C
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => A * x) B = (fun x => A * x) C
⊢ (fun x => det A • x) B = (fun x => det A • x) C
simp only at h ⊢
no goals
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : A * B = A * C
⊢ det A • B = det A • C
rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
  adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, ← mul_eq_mul A, h, mul_eq_mul]
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => x * A) B = (fun x => x * A) C
⊢ B = C
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsRightRegular A
intro B C h
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B ⬝ A = C ⬝ A
⊢ B = C
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => x * A) B = (fun x => x * A) C
⊢ B = C
simp only [mul_eq_mul] at h
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B ⬝ A = C ⬝ A
⊢ (fun x => det A • x) B = (fun x => det A • x) C
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B ⬝ A = C ⬝ A
⊢ B = C
refine' hA.matrix _
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B ⬝ A = C ⬝ A
⊢ det A • B = det A • C
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B ⬝ A = C ⬝ A
⊢ (fun x => det A • x) B = (fun x => det A • x) C
simp only
no goals
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B ⬝ A = C ⬝ A
⊢ det A • B = det A • C
rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
  mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]