Commit 2021-08-25 17:03 b364cfc3

feat(linear_algebra/basis): if R ≃ R', map a basis for R-module M to R'-module M (#8699) If R and R' are isomorphic rings that act identically on a module M, then a basis for M as R-module is also a basis for M as R'-module.