Documentation

Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

LiesOver instances for completions of number fields #

This file is deprecated: use AbsoluteValue.Completion.map and AbsoluteValue.Completion.algebraOfLiesOver instead, together with AbsoluteValue.Completion.algebra_eq_of_liesOver for uniqueness of the algebra structure.

source
@[deprecated AbsoluteValue.Completion.map (since := "2026-10-30")]
noncomputable def NumberField.LiesOver.completionMap {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] :
v.Completion →+* w.Completion

Alias of AbsoluteValue.Completion.map.

Equations
Instances For
    source
    @[deprecated AbsoluteValue.Completion.continuous_map (since := "2026-10-30")]
    theorem NumberField.LiesOver.continuous_completionMap {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) {L : Type u_2} [Field L] [Algebra K L] (w : AbsoluteValue L ℝ) [w.LiesOver v] :
    Continuous ⇑(AbsoluteValue.Completion.map v w)

    Alias of AbsoluteValue.Completion.continuous_map.

    source
    @[deprecated AbsoluteValue.Completion.map_coe (since := "2026-10-30")]
    theorem NumberField.LiesOver.completionMap_coe {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] (x : WithAbs ↑v) :
    (AbsoluteValue.Completion.map ↑v ↑w) ↑x = ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x)
    source
    @[instance_reducible]
    noncomputable def NumberField.LiesOver.instAlgebraCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] :
    Algebra v.Completion w.Completion

    If w lies over v, then w.Completion is a v.Completion-algebra.

    Equations
    Instances For
      source
      theorem NumberField.LiesOver.instIsScalarTowerCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] :
      IsScalarTower K v.Completion w.Completion
      source
      theorem NumberField.LiesOver.instContinuousSMulCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [w.LiesOver v] :
      ContinuousSMul v.Completion w.Completion