instCoeFun — Mathlib

English

Two linear isometry equivalences are equal if they agree on all vectors.

Русский

Две линейно изометрические эквивалентности равны, если они согласны на всех векторах.

LaTeX

$$$\\forall x: E,\\; e(x) = e'(x) \\Rightarrow e = e'$$$

Lean4

/-- Shortcut instance, saving 8.5% of compilation time in
`Mathlib/Analysis/InnerProductSpace/Adjoint.lean`.

(This instance was pinpointed by benchmarks; we didn't do an in depth investigation why it is
specifically needed.)
-/
instance instCoeFun : CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun _ ↦ E → E₂ :=
  ⟨DFunLike.coe⟩

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