English
This is the iff version of isDiag_fromBlocks: the block matrix A.fromBlocks B C D is diagonal exactly when A is diagonal, B=C=0, and D is diagonal.
Русский
Это эквивалентная формулировка isDiag_fromBlocks: диагональность матрицы fromBlocks эквивалентна diag(A) и B=C=0 и diag(D).
LaTeX
$$$\\forall {\\alpha} {n} {m} [Zero \\alpha] {A : Matrix m m \\alpha} {B : Matrix m n \\alpha} {C : Matrix n m \\alpha} {D : Matrix n n \\alpha},
(A.fromBlocks B C D).IsDiag \\iff A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag$$$
Lean4
/-- This is the `iff` version of `Matrix.IsDiag.fromBlocks`. -/
theorem isDiag_fromBlocks_iff [Zero α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
(A.fromBlocks B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag :=
by
constructor
· intro h
refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
· exact h (Sum.inl_injective.ne hij)
· exact h Sum.inl_ne_inr
· exact h Sum.inr_ne_inl
· exact h (Sum.inr_injective.ne hij)
· rintro ⟨ha, hb, hc, hd⟩
convert IsDiag.fromBlocks ha hd
