coe_coe — Mathlib

English

The function obtained by viewing e as an affine map and then as a function is equal to e itself.

Русский

Функция, полученная через представление e как аффиного отображения и затем как функции, равна e самому.

LaTeX

$$$((e : P_1 \to^{\mathrm{Affine}} P_2) : P_1 \to P_2) = e$$$

Lean4

@[norm_cast, simp]
theorem coe_coe (e : P₁ ≃ᵃ[k] P₂) : ((e : P₁ →ᵃ[k] P₂) : P₁ → P₂) = e :=
  rfl

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