coe_symm_mk — Mathlib

English

A canonical coercion of the symmetry of a constructed linear equivalence equals the inverse map inv_fun used in the symmetry construction.

Русский

К каноническому приведения симметрии построенного линейного эквивалента соответствует используемая в симметрии обратная функция.

LaTeX

$$coe_symm_mk: (constructed).symm = inv_fun$$

Lean4

/-- For a more powerful version, see `coe_symm_mk'`. -/
theorem coe_symm_mk [Module R M] [Module R M₂] {to_fun inv_fun map_add map_smul left_inv right_inv} :
    ⇑(⟨⟨⟨to_fun, map_add⟩, map_smul⟩, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂).symm = inv_fun :=
  rfl

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