equivOfEq — Mathlib

English

Given S = T between intermediate fields of F E, there is an algebra isomorphism between S and T determined by that equality.

Русский

При S = T между промежуточными полями F E существует алгебраическое изоморфирование между S и T, определяемое данному равенству.

LaTeX

$$$\\text{equivOfEq} : (S=T) \\Rightarrow S \\simeq_A^F T$$$

Lean4

/-- Construct an algebra isomorphism from an equality of intermediate fields. -/
@[simps! apply]
def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T :=
  Subalgebra.equivOfEq _ _ (congr_arg toSubalgebra h)

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