instSubfieldClass — Mathlib

English

Every intermediate field S carries the structure of a Subfield of L.

Русский

Каждое промежуточное поле S несет структуру подполя L.

LaTeX

$$$\text{IntermediateField}(K,L) \text{ is a } \text{SubfieldClass of } L$$$

Lean4

instance : SubfieldClass (IntermediateField K L) L
    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' _

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