instCoeHead — Mathlib

English

There is a natural CoeHead structure providing a canonical embedding of 𝓞K into K, i.e. 𝓞K can be viewed as a subobject of K via this inclusion.

Русский

Существует естественная структура CoeHead, обеспечивающая каноническое включение 𝓞K в K, то есть 𝓞K можно рассматривать как подобъект K через это включение.

LaTeX

$$$\\iota: \\mathcal{O}_K \\hookrightarrow K$$$

Lean4

/-- This instance has to be `CoeHead` because we only want to apply it from `𝓞 K` to `K`. -/
instance : CoeHead (𝓞 K) K :=
  ⟨val⟩

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