mathlib3

bda3a79e - feat(algebra/algebra): lemmas connecting `basis ι R A`, `no_zero_smul_divisors R A` and `injective (algebra_map R A)`

feat(algebra/algebra): lemmas connecting `basis ι R A`, `no_zero_smul_divisors R A` and `injective (algebra_map R A)` Additions: * `basis.algebra_map_injective` * `no_zero_smul_divisors.algebra_map_injective` * `no_zero_smul_divisors.iff_algebra_map_injective` Renamed: * `algebra.no_zero_smul_divisors.of_algebra_map_injective` → `no_zero_smul_divisors.of_algebra_map_injective`