Commit 2021-09-07 23:04 dcd87822

feat(algebra/algebra): lemmas connecting basis ι R A, no_zero_smul_divisors R A and injective (algebra_map R A) (#9039) 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