toField — Mathlib

English

A subfield inherits a field structure.

Русский

Подполе наследует структуру поля.

LaTeX

$$instance toField {K} [Field K] (s : Subfield K) : Field (Subtype (SetLike.mem s))$$

Lean4

/-- A subfield inherits a field structure -/
instance toField {K} [Field K] (s : Subfield K) : Field s :=
  fast_instance%Subtype.coe_injective.field ((↑) : s → K) rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
      (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ ↦ rfl) (fun _ => rfl) (fun _ => rfl) (fun _ ↦ rfl) fun _ => rfl

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