Def linear_equiv.congr_right
Modification history
2021-08-21 17:31
src/linear_algebra/basic.lean
chore(linear_algebra): remove `→ₗ` notation where the ring is not specified (#8778) …
Modified linear_equiv.congr_rightView on Github →2020-12-15 17:57
src/linear_algebra/basic.lean
ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter (#5330) …
Modified linear_equiv.congr_rightView on Github →2020-03-22 04:38
src/linear_algebra/basic.lean
fix(linear_algebra/basic): make R explicit in linear_equiv.refl (#2161) …
Modified linear_equiv.congr_rightView on Github →2019-10-10 11:14
src/linear_algebra/basic.lean
chore(linear_algebra): rename type variables (#1521) …
Modified linear_equiv.congr_rightView on Github →2019-08-16 10:20
src/linear_algebra/basic.lean
feat(linear_algebra/matrix): linear maps are linearly equivalent to matrices (#1310) …
Modified linear_equiv.congr_rightView on Github →