chore(data/matrix/block): Do not print matrix.from_blocks with dot …

…notation (#12774)

`A.from_blocks B C D` is weird and asymmetric compared to `from_blocks A B C D`. In future we might want to introduce notation.

src/data/matrix/block.lean

@@ -28,6 +28,7 @@ section block_matrices
 
 /-- We can form a single large matrix by flattening smaller 'block' matrices of compatible
 dimensions. -/
+@[pp_nodot]
 def from_blocks (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) :
   matrix (n ⊕ o) (l ⊕ m) α :=
 sum.elim (λ i, sum.elim (A i) (B i))