mathlib3

ae6d77ba - feat(linear_algebra/free_module): a set of linearly independent vectors over a ring S is also linearly independent over a subring R of S (#6993)

feat(linear_algebra/free_module): a set of linearly independent vectors over a ring S is also linearly independent over a subring R of S (#6993) Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60algebra_map.2Einjective.2Elinear_independent.60