noncomputable def InfinitePlaceBaseChange.ringEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) : TensorProduct K L v.Completion ≃+* ((w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)