commRing — Mathlib

English

If R is a commutative ring, TopologicalRing structure on R lifts to a Commutative Ring structure on Completion R.

Русский

Если R — коммутативное кольцо, топологическая структура на R переносится на коммутативное кольцо на Completion R.

LaTeX

$$$$ \mathrm{CommRing}(\mathrm{Completion} R) $$$$

Lean4

instance commRing : CommRing (Completion R) :=
  { Completion.ring with
    mul_comm := fun a b =>
      Completion.induction_on₂ a b (isClosed_eq (continuous_fst.mul continuous_snd) (continuous_snd.mul continuous_fst))
        fun a b => by rw [← coe_mul, ← coe_mul, mul_comm] }

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