instInvCompletion — Mathlib

English

In the completed field hat K, the inverse of zero is defined to be zero. That is, the inverse operation satisfies 0^{-1} = 0.

Русский

В дополнении hat K обратная к нулю определяется как ноль: 0^{-1} = 0.

LaTeX

$$$(0)^{-1} = 0$$$

Lean4

/-- The value of `hat_inv` at zero is not really specified, although it's probably zero.
Here we explicitly enforce the `inv_zero` axiom.
-/
instance instInvCompletion : Inv (hat K) :=
  ⟨fun x => if x = 0 then 0 else hatInv x⟩

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