coe_equivInteger_apply — Mathlib

English

Under the isomorphism, the image of a ∈ A coincides with its embedding in K; i.e., (equivInteger A K a) coerced to K equals algebraMap A K a.

Русский

При помощи изоморфизма образ элемента a ∈ A совпадает с его вложением в K; то есть (equivInteger A K a) неявно как элемент K равен algebraMap A K a.

LaTeX

$$$ (\\operatorname{equivInteger} A K\\ a) \\\\( : K) = \\operatorname{algebraMap} A K\\ a $$$

Lean4

@[simp]
theorem coe_equivInteger_apply (a : A) : (equivInteger A K a : K) = algebraMap A K a :=
  rfl

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