Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-28 09:53 162d83fc

View on Github →

chore(data/matrix/basic): square matrices over a non-unital ring form a non-unital ring (#12913)

Estimated changes

Modified src/data/matrix/basic.lean

modified theorem matrix.conj_transpose_neg