English
If α is a ring with a uniform structure, then the completion α has a ring structure extending α.
Русский
Если α — кольцо с равномерной структурой, то дополнение α имеет кольцо, расширяющее α.
LaTeX
$$$\\mathrm{Ring}(\\mathrm{Completion}(\\alpha))$$$
Lean4
instance ring : Ring (Completion α) :=
{ AddMonoidWithOne.unary, (inferInstanceAs (AddCommGroup (Completion α))), (inferInstanceAs (Mul (Completion α))),
(inferInstanceAs
(One
(Completion
α))) with
zero_mul := fun a =>
Completion.induction_on a (isClosed_eq (continuous_const.mul continuous_id) continuous_const) fun a => by
rw [← coe_zero, ← coe_mul, zero_mul]
mul_zero := fun a =>
Completion.induction_on a (isClosed_eq (continuous_id.mul continuous_const) continuous_const) fun a => by
rw [← coe_zero, ← coe_mul, mul_zero]
one_mul := fun a =>
Completion.induction_on a (isClosed_eq (continuous_const.mul continuous_id) continuous_id) fun a => by
rw [← coe_one, ← coe_mul, one_mul]
mul_one := fun a =>
Completion.induction_on a (isClosed_eq (continuous_id.mul continuous_const) continuous_id) fun a => by
rw [← coe_one, ← coe_mul, mul_one]
mul_assoc := fun a b c =>
Completion.induction_on₃ a b c
(isClosed_eq
((continuous_fst.mul (continuous_fst.comp continuous_snd)).mul (continuous_snd.comp continuous_snd))
(continuous_fst.mul ((continuous_fst.comp continuous_snd).mul (continuous_snd.comp continuous_snd))))
fun a b c => by rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
left_distrib := fun a b c =>
Completion.induction_on₃ a b c
(isClosed_eq
(continuous_fst.mul
(Continuous.add (continuous_fst.comp continuous_snd) (continuous_snd.comp continuous_snd)))
(Continuous.add (continuous_fst.mul (continuous_fst.comp continuous_snd))
(continuous_fst.mul (continuous_snd.comp continuous_snd))))
fun a b c => by rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
right_distrib := fun a b c =>
Completion.induction_on₃ a b c
(isClosed_eq
((Continuous.add continuous_fst (continuous_fst.comp continuous_snd)).mul
(continuous_snd.comp continuous_snd))
(Continuous.add (continuous_fst.mul (continuous_snd.comp continuous_snd))
((continuous_fst.comp continuous_snd).mul (continuous_snd.comp continuous_snd))))
fun a b c => by rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul] }
