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

Commit
3 years ago
chore(data/matrix/basic): square matrices over a non-unital ring form a non-unital ring (#12913)
Author
Parents
Loading