English
The Cauchy completion with respect to abv forms a division ring, equipped with the standard interpretations of inv, mul, and div.
Русский
Дополнение Коши относительно abv образует деление кольцо с нормальным определением обратного, умножения и деления.
LaTeX
$$DivisionRing (CauSeq.Completion.Cauchy abv)$$
Lean4
/-- The Cauchy completion forms a division ring. -/
noncomputable instance divisionRing : DivisionRing (Cauchy abv)
where
inv_zero := inv_zero
mul_inv_cancel _ := CauSeq.Completion.mul_inv_cancel
nnqsmul := (· • ·)
qsmul := (· • ·)
nnratCast_def q := by simp_rw [← ofRat_nnratCast, NNRat.cast_def, ofRat_div, ofRat_natCast]
ratCast_def q := by rw [← ofRat_ratCast, Rat.cast_def, ofRat_div, ofRat_natCast, ofRat_intCast]
nnqsmul_def _ x := Quotient.inductionOn x fun _ ↦ congr_arg mk <| ext fun _ ↦ NNRat.smul_def _ _
qsmul_def _ x := Quotient.inductionOn x fun _ ↦ congr_arg mk <| ext fun _ ↦ Rat.smul_def _ _
