[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i j : n
⊢ diagonal (diag A) i j = A i j
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case inl
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i : n
⊢ diagonal (diag A) i i = A i i
[PROOFSTEP]
rw [diagonal_apply_eq, diag]
[GOAL]
case inr
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i j : n
hij : i ≠ j
⊢ diagonal (diag A) i j = A i j
[PROOFSTEP]
rw [diagonal_apply_ne _ hij, h hij]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : IsDiag A
f : α → β
hf : f 0 = 0
⊢ IsDiag (Matrix.map A f)
[PROOFSTEP]
intro i j h
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : IsDiag A
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ Matrix.map A f i j = 0
[PROOFSTEP]
simp [ha h, hf]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : AddGroup α
A : Matrix n n α
ha : IsDiag A
⊢ IsDiag (-A)
[PROOFSTEP]
intro i j h
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : AddGroup α
A : Matrix n n α
ha : IsDiag A
i j : n
h : i ≠ j
⊢ (-A) i j = 0
[PROOFSTEP]
simp [ha h]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
⊢ IsDiag (A + B)
[PROOFSTEP]
intro i j h
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
i j : n
h : i ≠ j
⊢ (A + B) i j = 0
[PROOFSTEP]
simp [ha h, hb h]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : AddGroup α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
⊢ IsDiag (A - B)
[PROOFSTEP]
intro i j h
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : AddGroup α
A B : Matrix n n α
ha : IsDiag A
hb : IsDiag B
i j : n
h : i ≠ j
⊢ (A - B) i j = 0
[PROOFSTEP]
simp [ha h, hb h]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : IsDiag A
⊢ IsDiag (k • A)
[PROOFSTEP]
intro i j h
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : IsDiag A
i j : n
h : i ≠ j
⊢ (k • A) i j = 0
[PROOFSTEP]
simp [ha h]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Semiring α
inst✝ : StarRing α
A : Matrix n n α
ha : IsDiag Aᴴ
⊢ IsDiag A
[PROOFSTEP]
convert ha.conjTranspose
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝¹ : Semiring α
inst✝ : StarRing α
A : Matrix n n α
ha : IsDiag Aᴴ
⊢ A = Aᴴᴴ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
⊢ IsDiag (kroneckerMap (fun x x_1 => x * x_1) A B)
[PROOFSTEP]
rintro ⟨a, b⟩ ⟨c, d⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
[PROOFSTEP]
simp only [Prod.mk.inj_iff, Ne.def, not_and_or] at h 
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
[PROOFSTEP]
cases' h with hac hbd
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
[PROOFSTEP]
simp [hA hac]
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : IsDiag A
hB : IsDiag B
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x x_1 => x * x_1) A B (a, b) (c, d) = 0
[PROOFSTEP]
simp [hB hbd]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
⊢ IsSymm A
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
⊢ Aᵀ i j = A i j
[PROOFSTEP]
by_cases g : i = j
[GOAL]
case pos
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
g : i = j
⊢ Aᵀ i j = A i j
[PROOFSTEP]
rw [g, transpose_apply]
[GOAL]
case neg
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j
[PROOFSTEP]
simp [h g, h (Ne.symm g)]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 0 D)
[PROOFSTEP]
rintro (i | i) (j | j) hij
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i j : m
hij : Sum.inl i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0
[PROOFSTEP]
exact ha (ne_of_apply_ne _ hij)
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i : m
j : n
hij : Sum.inl i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inr j) = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i : n
j : m
hij : Sum.inr i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inl j) = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
D : Matrix n n α
ha : IsDiag A
hd : IsDiag D
i j : n
hij : Sum.inr i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0
[PROOFSTEP]
exact hd (ne_of_apply_ne _ hij)
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag (fromBlocks A B C D) ↔ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag (fromBlocks A B C D) → IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
⊢ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D
[PROOFSTEP]
refine' ⟨fun i j hij => _, ext fun i j => _, ext fun i j => _, fun i j hij => _⟩
[GOAL]
case mp.refine'_1
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i j : m
hij : i ≠ j
⊢ A i j = 0
[PROOFSTEP]
exact h (Sum.inl_injective.ne hij)
[GOAL]
case mp.refine'_2
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i : m
j : n
⊢ B i j = OfNat.ofNat 0 i j
[PROOFSTEP]
exact h Sum.inl_ne_inr
[GOAL]
case mp.refine'_3
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i : n
j : m
⊢ C i j = OfNat.ofNat 0 i j
[PROOFSTEP]
exact h Sum.inr_ne_inl
[GOAL]
case mp.refine'_4
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : IsDiag (fromBlocks A B C D)
i j : n
hij : i ≠ j
⊢ D i j = 0
[PROOFSTEP]
exact h (Sum.inr_injective.ne hij)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ IsDiag A ∧ B = 0 ∧ C = 0 ∧ IsDiag D → IsDiag (fromBlocks A B C D)
[PROOFSTEP]
rintro ⟨ha, hb, hc, hd⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
ha : IsDiag A
hb : B = 0
hc : C = 0
hd : IsDiag D
⊢ IsDiag (fromBlocks A B C D)
[PROOFSTEP]
convert IsDiag.fromBlocks ha hd
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : IsSymm (Matrix.fromBlocks A 0 C D)
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 C D)
[PROOFSTEP]
rw [← (isSymm_fromBlocks_iff.1 h).2.1]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : IsSymm (Matrix.fromBlocks A 0 C D)
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 0ᵀ D)
[PROOFSTEP]
exact ha.fromBlocks hd
