coe_symm_mk' — Mathlib

English

A variant of how the inverse of a constructed linear equivalence has its function equal to the provided inv_fun.

Русский

Вариант того, как обратная к сконструированному линейному эквиваленту действует как заданная inv_fun.

LaTeX

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

Lean4

@[simp]
theorem coe_symm_mk' [Module R M] [Module R M₂] {f inv_fun left_inv right_inv} :
    ⇑(⟨f, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂).symm = inv_fun :=
  rfl

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