Theorems · Theorem · number theory

NumberField.InfinitePlace.Completion.algebraMap_toCompletion

∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (R : Type u_2) [inst_1 : CommSemiring R]
  [inst_2 : Algebra R (WithAbs ↑v)] [inst_3 : UniformContinuousConstSMul R (WithAbs ↑v)] (r : R),
  ((algebraMap R v.Completion) r).toCompletion = (algebraMap R (↑v).Completion) r

Defined in

Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Cited by

1 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCommSemiringAlgebraUniformContinuousConstSMul