Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix.sub_right

Modification history

2018-11-05 13:47
ring_theory/matrix.lean
feat(ring_theory/matrix): add minor, sub_[left|right|up|down], sub_[left|right]_[up][down] (#389) …
Added matrix.sub_rightView on Github →