English
There is a canonical inversion operation making CauSeq.Completion.Cauchy abv into a division-like structure, with inv defined compatibly with 0.
Русский
Существует каноническое взятие обратного, превращающее CauSeq.Completion.Cauchy abv в структуру, аналогичную делению, с определением обратного относительно 0.
LaTeX
$$$\text{instInvCauchy} : Inv (CauSeq.Completion.Cauchy abv)$$$
Lean4
noncomputable instance : Inv (Cauchy abv) :=
⟨fun x =>
(Quotient.liftOn x fun f => mk <| if h : LimZero f then 0 else inv f h) fun f g fg =>
by
have := limZero_congr fg
by_cases hf : LimZero f
· simp [hf, this.1 hf]
· have hg := mt this.2 hf
simp only [hf, dite_false, hg]
have If : mk (inv f hf) * mk f = 1 := mk_eq.2 (inv_mul_cancel hf)
have Ig : mk (inv g hg) * mk g = 1 := mk_eq.2 (inv_mul_cancel hg)
have Ig' : mk g * mk (inv g hg) = 1 := mk_eq.2 (mul_inv_cancel hg)
rw [mk_eq.2 fg, ← Ig] at If
rw [← mul_one (mk (inv f hf)), ← Ig', ← mul_assoc, If, mul_assoc, Ig', mul_one]⟩
