coe_doubleDualEquiv — Mathlib

English

The coe projection of doubleDualEquiv equals the identity embedding: the function coe of doubleDualEquiv is equal to doubleDualEmb.

Русский

Проекция коe двойной дуальности совпадает с тождественным вложением: коe doubleDualEquiv равняется doubleDualEmb.

LaTeX

$$$ \text{coe}(\text{doubleDualEquiv}) = \text{doubleDualEmb} $$$

Lean4

@[simp]
theorem coe_doubleDualEquiv : ⇑(doubleDualEquiv : α ≃+ AddChar (AddChar α ℂ) ℂ) = doubleDualEmb :=
  rfl

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