instSubfieldClass — Mathlib

English

There is a canonical instance that endows Subfield K with a SubfieldClass structure, aligning its data with field-like properties.

Русский

Существует каноничный экземпляр, доказывающий, что Subfield K имеет структуру SubfieldClass, согласующую поля с свойствами поля.

LaTeX

$$$\text{Subfield} \text{ has a } SubfieldClass \text{ instance.}$$$

Lean4

instance : SubfieldClass (Subfield K) K where
  add_mem {s} := s.add_mem'
  zero_mem s := s.zero_mem'
  neg_mem {s} := s.neg_mem'
  mul_mem {s} := s.mul_mem'
  one_mem s := s.one_mem'
  inv_mem {s} := s.inv_mem' _

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