doubleDualEquiv_symm_doubleDualEmb_apply

English

The symmetry relation holds: doubleDualEquiv.symm (doubleDualEmb a) = a for all a ∈ AddChar(AddChar α ℂ) ℂ.

Русский

Симметрическое равенство: doubleDualEquiv.symm (doubleDualEmb a) = a для всех a ∈ AddChar(AddChar α ℂ) ℂ.

LaTeX

$$$ doubleDualEquiv.symm (doubleDualEmb a) = a $$$

Lean4

@[simp]
theorem doubleDualEquiv_symm_doubleDualEmb_apply (a : AddChar (AddChar α ℂ) ℂ) :
    doubleDualEquiv.symm (doubleDualEmb a) = a :=
  doubleDualEquiv.symm_apply_apply _

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