∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x y : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)),
  (((UniformSpace.Completion.mapRingEquiv
                  (WithVal.equivWithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)
                    (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)))
                  ⋯ ⋯).restrict
              (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)
              (Valued.integer (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)).Completion) ⋯).trans
          PadicInt.withValIntegersRingEquiv).toFun
      (x * y) =
    (((UniformSpace.Completion.mapRingEquiv
                    (WithVal.equivWithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)
                      (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)))
                    ⋯ ⋯).restrict
                (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)
                (Valued.integer (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)).Completion) ⋯).trans
            PadicInt.withValIntegersRingEquiv).toFun
        x *
      (((UniformSpace.Completion.mapRingEquiv
                    (WithVal.equivWithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v)
                      (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)))
                    ⋯ ⋯).restrict
                (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)
                (Valued.integer (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v)).Completion) ⋯).trans
            PadicInt.withValIntegersRingEquiv).toFun
        y