mathlib3
36649f8b - chore(linear_algebra/basic): add linear_map.one_eq_id (#7063)

Commit

4 years ago

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

Author

eric-wieser

Parents