English
There exists a random R-algebra isomorphism between L and M, where L is an algebraic closure of R and M is an algebraic closure of an algebraic extension of R.
Русский
Существет произвольный R-алгебраический изоморфизм между L и M, где L — алгебраическое замыкание R, а M — алгебраическое замыкание алгебраического расширения R.
LaTeX
$$$\\exists\\, \\phi: L \\cong_R M$ given the appropriate algebraic closure hypotheses.$$
Lean4
/-- A (random) isomorphism between an algebraic closure of `R` and an algebraic closure of
an algebraic extension of `R` -/
noncomputable def equivOfAlgebraic' [Nontrivial S] [NoZeroSMulDivisors R S] [Algebra.IsAlgebraic R L] : L ≃ₐ[R] M :=
by
have : NoZeroSMulDivisors R L := NoZeroSMulDivisors.trans_faithfulSMul R S L
have : IsAlgClosure R L :=
{ isAlgClosed := IsAlgClosure.isAlgClosed S
isAlgebraic := ‹_› }
exact IsAlgClosure.equiv _ _ _
