English
If E is an F-algebra and there exists an injective F-linear map b : F → E, then the canonical algebra map algebraMap F E is injective.
Русский
Если E — F-alгебра и существует инъективное F-линейное отображение b : F → E, то каноническое отображение algebraMap F E инъективно.
LaTeX
$$$\\text{If } b:\\; F \\rightarrow_{F} E\\text{ is injective, then }\\operatorname{algebraMap}_{F\\to E} \\text{ is injective}.$$$
Lean4
/-- If `E` is an `F`-algebra, and there exists an injective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also injective. -/
theorem injective_algebraMap_of_linearMap (hb : Injective b) : Injective (algebraMap F E) := fun x y e ↦
hb <| by
rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul, map_smul, map_smul, Algebra.smul_def, Algebra.smul_def,
e]
