English
If b is bijective, then the algebra map algebraMap F E is bijective.
Русский
Если линейное отображение b биективно, то алгебраMap F E биективна.
LaTeX
$$$\\text{If } b\\text{ is bijective, then } algebraMap F E\\text{ is bijective.}$$$
Lean4
/-- If `E` is an `F`-algebra, and there exists a bijective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also bijective.
NOTE: The same result can also be obtained if there are two `F`-linear maps from `F` to `E`,
one is injective, the other one is surjective. In this case, use
`injective_algebraMap_of_linearMap` and `surjective_algebraMap_of_linearMap` separately. -/
theorem bijective_algebraMap_of_linearMap (hb : Bijective b) : Bijective (algebraMap F E) :=
⟨injective_algebraMap_of_linearMap b hb.1, surjective_algebraMap_of_linearMap b hb.2⟩
