adjoinRootAlgEquiv_symm_apply_eq_mk

English

For any a in S, h.adjoinRootAlgEquiv.symm(a) equals AdjoinRoot.mk f (h.repr a).

Русский

Для каждого a∈S обратное отображение h.adjoinRootAlgEquiv.symm(a) равно AdjoinRoot.mk f (h.repr a).

LaTeX

$$$h.adjoinRootAlgEquiv.symm(a) = \operatorname{AdjoinRoot.mk} f (h.repr(a))$$$

Lean4

theorem adjoinRootAlgEquiv_symm_apply_eq_mk (a : S) : h.adjoinRootAlgEquiv.symm a = AdjoinRoot.mk f (h.repr a) := by
  rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]

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