equivOfEquiv

Mathlib.FieldTheory.IsAlgClosed.Basic

URI: https://scilib.ai/kg/mathlib#IsAlgClosure.equivOfEquiv

English

Algebraic closures of isomorphic base fields are isomorphic.

Русский

Алгебраические замыкания изоморфных базовых полей изоморфны друг другу.

LaTeX

$$If S ≃+* R and L, M are algebraic closures over S and R respectively, then L ≃+* M.$$

Lean4

/-- Algebraic closure of isomorphic fields are isomorphic -/
noncomputable def equivOfEquiv (hSR : S ≃+* R) : L ≃+* M :=
  equivOfEquivAux L M hSR

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru