Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 13:47 279b9eda

View on Github →

feat(ring_theory/matrix): add minor, sub_[left|right|up|down], sub_[left|right]_[up][down] (#389) Also add fin.nat_add.

Estimated changes

Modified data/fin.lean

added def fin.nat_add

Modified ring_theory/matrix.lean

added def matrix.minor

added def matrix.sub_down

added def matrix.sub_down_left

added def matrix.sub_down_right

added def matrix.sub_left

added def matrix.sub_right

added def matrix.sub_up

added def matrix.sub_up_left

added def matrix.sub_up_right