coe_mk — Mathlib

English

If you build a semilinear equivalence from its data, the underlying function of that constructed object is exactly the given function.

Русский

Если построить семилинейную эквивалентность из её данных, ее базовая функция совпадает с заданной функцией.

LaTeX

$$coe_mk {f invFun left_inv right_inv} : ((⟨f, invFun, left_inv, right_inv⟩ : M ≃ₛₗ[σ] M₂) : M → M₂) = f$$

Lean4

@[simp]
theorem coe_mk {f invFun left_inv right_inv} : ((⟨f, invFun, left_inv, right_inv⟩ : M ≃ₛₗ[σ] M₂) : M → M₂) = f :=
  rfl

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