bijective_algebraMap_of_linearEquiv

English

If there is a bijective F-linear equivalence F ≃ₗ[F] E, then algebraMap F E is bijective.

Русский

Если существует биективное F-линейное эквивалентное отображение F ≃ₗ[F] E, то алгебраMap F E биективна.

LaTeX

$$$\\text{If } b:\\; F \\simeq_{\\!F} E\\text{ is bijective, then } algebraMap F E\\text{ is bijective.}$$$

Lean4

/-- If `E` is an `F`-algebra, there exists an `F`-linear isomorphism from `F` to `E` (namely,
`E` is a free `F`-module of rank one), then the algebra map from `F` to `E` is bijective. -/
theorem bijective_algebraMap_of_linearEquiv (b : F ≃ₗ[F] E) : Bijective (algebraMap F E) :=
  bijective_algebraMap_of_linearMap _ b.bijective

Похожие утверждения