mathlib
dd5e779e - fix(linear_algebra/basic): fix incorrect namespaces (#8757)

Commit
4 years ago
fix(linear_algebra/basic): fix incorrect namespaces (#8757) Previously there were names in the `linear_map` namespace which were about `linear_equiv`s. This moves: * `linear_map.fun_congr_left` to `linear_equiv.fun_congr_left` * `linear_map.automorphism_group` to `linear_equiv.automorphism_group` * `linear_map.automorphism_group.to_linear_map_monoid_hom` to `linear_equiv.automorphism_group.to_linear_map_monoid_hom`
Author
Parents
Loading