Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-19 14:31 dd5e779e

View on Github →

fix(linear_algebra/basic): fix incorrect namespaces (#8757) Previously there were names in the linear_map namespace which were about linear_equivs. 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

Estimated changes