adjoinRootAlgEquiv_apply_eq_map — Mathlib

English

For any a in AdjoinRoot f, h.adjoinRootAlgEquiv(a) equals h.map of the surjective preimage chosen by mk_surjective.

Русский

Для элемента a∈AdjoinRoot f выполняется равенство h.adjoinRootAlgEquiv(a) = h.map(AdjoinRoot.mk_surjective(a).choose).

LaTeX

$$$h.adjoinRootAlgEquiv a = h.map(\operatorname{AdjoinRoot.mk\_surjective}(a).choose$$$

Lean4

theorem adjoinRootAlgEquiv_apply_eq_map (a : AdjoinRoot f) :
    h.adjoinRootAlgEquiv a = h.map (AdjoinRoot.mk_surjective a).choose := by
  rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]

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