compatibleRingOfModelField — Mathlib

English

A locally defined field structure is transported to Type K that already has ring operations, turning it into a field.

Русский

Локальная структура поля переносится на тип K, который уже имеет кольцевые операции, превращая его в поле.

LaTeX

$$$\text{fieldOfModelField}(K) \Rightarrow \text{Field}(K)$$$

Lean4

/-- The instances given by `fieldOfModelField` are compatible with the `Language.ring.Structure`
instance on `K`. This instance is to be used on models for the language of fields that do
not already have the ring operations on the Type.

Always add `fieldOfModelField` as a local instance first before using this instance.
-/
noncomputable abbrev compatibleRingOfModelField (K : Type*) [Language.ring.Structure K] [Theory.field.Model K] :
    CompatibleRing K :=
  compatibleRingOfRingStructure K

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