algebraMap_equivMaximalRealSubfield_symm_apply

English

The algebra map from F to K, composed with the inverse of the real-subfield equivalence, coincides with the trivial embedding on the real subfield; in short, algebraMap F K (equivMaximalRealSubfield(F,K)^{-1}(x)) = algebraMap (maximalRealSubfield(K)) K (x).

Русский

Вложение через алгебраическое отображение совпадает с вложением через максимальное действительное подполе: algebraMap F K ((equivMaxRealSubfield F K)^{-1}(x)) = algebraMap (maximalRealSubfield K) K x.

LaTeX

$$$\\mathrm{algebraMap}_{F,K}\\big((\\mathrm{equivMaximalRealSubfield}(F,K))^{-1}(x)\\big) = \\mathrm{algebraMap}_{\\maxRealSub(K)\\to K}(x)$$$

Lean4

@[simp]
theorem algebraMap_equivMaximalRealSubfield_symm_apply (x : maximalRealSubfield K) :
    algebraMap F K ((CMExtension.equivMaximalRealSubfield F K).symm x) = algebraMap (maximalRealSubfield K) K x := by
  simpa using (equivMaximalRealSubfield_apply F K ((equivMaximalRealSubfield F K).symm x)).symm

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