norm_infinitePlace_completion — Mathlib

English

In the real-case, ratCast_equiv expresses that casting via WithAbs equiv matches the completion embedding.

Русский

В вещественном случае ratCast_equiv показывает соответствие между приведением через WithAbs и вложением в дополнение.

LaTeX

$$Rat.cast (WithAbs.equiv _ x) = (x : v.Completion)$$

Lean4

theorem norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) : ‖(x : v.Completion)‖ = |x| := by
  rw [← (WithAbs.equiv v.1).apply_symm_apply x, WithAbs.ratCast_equiv, norm_coe, (WithAbs.equiv v.1).apply_symm_apply,
    Rat.infinitePlace_apply]

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