Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 10:30 36649f8b

View on Github →

chore(linear_algebra/basic): add linear_map.one_eq_id (#7063) Cherry-picked from #4773

Estimated changes

added theorem linear_map.one_eq_id