English
If f is a bijective algebra homomorphism A1 →ₐ[R] A2, then there exists an algebra equivalence A1 ≃ₐ[R] A2 whose underlying map is f; i.e., a bijective algebra homomorphism is an algebra isomorphism.
Русский
Если f — биективный алгебраический гомоморфизм A1 →ₐ[R] A2, то существует алгебраическое эквивалентное отображение A1 ≃ₐ[R] A2, чьё основание совпадает с f; то есть биективный алгебраический гомоморфизм является алгебраическим изоморфизмом.
LaTeX
$$$\\exists e : A_1 \\simeq_{R} A_2 \\;\\text{с} \\; e.toAlgHom = f$$$
Lean4
/-- Promotes a bijective algebra homomorphism to an algebra equivalence. -/
noncomputable def ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : A₁ ≃ₐ[R] A₂ :=
{ RingEquiv.ofBijective (f : A₁ →+* A₂) hf, f with }
