Skip to content

Commit

Permalink
style(Data/Matrix/Block): define Matrix.fromBlocks more esthetically (
Browse files Browse the repository at this point in the history
  • Loading branch information
madvorak committed Nov 21, 2024
1 parent 439565f commit b513113
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Matrix/Block.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ dimensions. -/
@[pp_nodot]
def fromBlocks (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
Matrix (n ⊕ o) (l ⊕ m) α :=
of <| Sum.elim (fun i => Sum.elim (A i) (B i)) fun i => Sum.elim (C i) (D i)
of <| Sum.elim (fun i => Sum.elim (A i) (B i)) (fun j => Sum.elim (C j) (D j))

@[simp]
theorem fromBlocks_apply₁₁ (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
Expand Down

0 comments on commit b513113

Please sign in to comment.