instField — Mathlib

English

The center of a division ring is a field.

Русский

Центр деление кольца является полем.

LaTeX

$$center K is a Field$$

Lean4

instance instField : Field (center K)
    where
  inv a := ⟨a⁻¹, Set.inv_mem_center a.prop⟩
  mul_inv_cancel _ ha := Subtype.ext <| mul_inv_cancel₀ <| Subtype.coe_injective.ne ha
  div a b := ⟨a / b, Set.div_mem_center a.prop b.prop⟩
  div_eq_mul_inv _ _ := Subtype.ext <| div_eq_mul_inv _ _
  inv_zero := Subtype.ext inv_zero
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

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