instField — Mathlib

English

The completion hat K of a field K carries a full field structure compatible with the ambient uniform space.

Русский

Дополнение hat K поля K образует полное поле, совместимое с окружающей униформной структурой.

LaTeX

$$$\hat K \text{ is a field}$$$

Lean4

instance instField : Field (hat K)
    where
  mul_inv_cancel := fun x x_ne => by simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne]
  inv_zero := by
    simp only [Inv.inv, ite_true]
      -- TODO: use a better defeq

  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

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