intermediateFieldMap_symm_apply_coe

English

For e an equivalence, a ∈ E.map e, the symmetry map sends a to e.symm(a) when coerced.

Русский

Для эквивалентности e и a ∈ E.map e, симметрическое отображение переводит a в e.symm(a) при приводе к виду.

LaTeX

$$$↑((intermediateFieldMap e E).symm a) = e.symm a$$$

Lean4

theorem intermediateFieldMap_symm_apply_coe (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E.map e.toAlgHom) :
    ↑((intermediateFieldMap e E).symm a) = e.symm a :=
  rfl

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