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`

src/algebra/algebra/basic.lean

@@ -323,30 +323,59 @@ begin
       mul_assoc, ih, ←mul_assoc], }
 end
 
+end ring
+
+end algebra
+
+namespace no_zero_smul_divisors
+
+variables {R A : Type*}
+
+open algebra
+
+section ring
+
+variables [comm_ring R]
+
 /-- If `algebra_map R A` is injective and `A` has no zero divisors,
 `R`-multiples in `A` are zero only if one of the factors is zero.
 
 Cannot be an instance because there is no `injective (algebra_map R A)` typeclass.
 -/
-lemma no_zero_smul_divisors.of_algebra_map_injective
+lemma of_algebra_map_injective
   [semiring A] [algebra R A] [no_zero_divisors A]
   (h : function.injective (algebra_map R A)) : no_zero_smul_divisors R A :=
 ⟨λ c x hcx, (mul_eq_zero.mp ((smul_def c x).symm.trans hcx)).imp_left
   ((algebra_map R A).injective_iff.mp h _)⟩
 
+variables (R A)
+lemma algebra_map_injective [ring A] [nontrivial A]
+  [algebra R A] [no_zero_smul_divisors R A] :
+  function.injective (algebra_map R A) :=
+suffices function.injective (λ (c : R), c • (1 : A)),
+by { convert this, ext, rw [algebra.smul_def, mul_one] },
+smul_left_injective R one_ne_zero
+
+variables {R A}
+lemma iff_algebra_map_injective [domain A] [algebra R A] :
+  no_zero_smul_divisors R A ↔ function.injective (algebra_map R A) :=
+⟨@@no_zero_smul_divisors.algebra_map_injective R A _ _ _ _,
+ no_zero_smul_divisors.of_algebra_map_injective⟩
+
 end ring
 
 section field
 
 variables [field R] [semiring A] [algebra R A]
 
 @[priority 100] -- see note [lower instance priority]
-instance [nontrivial A] [no_zero_divisors A] : no_zero_smul_divisors R A :=
+instance algebra.no_zero_smul_divisors [nontrivial A] [no_zero_divisors A] :
+  no_zero_smul_divisors R A :=
 no_zero_smul_divisors.of_algebra_map_injective (algebra_map R A).injective
 
 end field
 
-end algebra
+end no_zero_smul_divisors
 
 namespace opposite
 

src/ring_theory/algebra_tower.lean

@@ -200,6 +200,12 @@ begin
   { simp [hi] },
 end
 
+lemma basis.algebra_map_injective {ι : Type v₁} [no_zero_divisors R] [nontrivial S]
+  (b : basis ι R S) :
+  function.injective (algebra_map R S) :=
+have no_zero_smul_divisors R S := b.no_zero_smul_divisors,
+by exactI no_zero_smul_divisors.algebra_map_injective R S
+
 end ring
 
 section artin_tate