toField — Mathlib

English

A subfield carries a natural field structure; i.e., it is a field in its own right.

Русский

Подполе обладает естественной структурой поля; то есть это поле само по себе.

LaTeX

$$$s\text{ is a field}$$$

Lean4

/-- A subfield of a field inherits a field structure -/
instance (priority := 75) toField {K} [Field K] [SetLike S K] [SubfieldClass S K] (s : S) : 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) (coe_nnqsmul _) (coe_qsmul _)
      (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)

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