continuous_normAtPlace — Mathlib

English

For every place w, the local norm map at w is a continuous function on the mixed space.

Русский

Для каждого места w локальная норма на этом месте является непрерывной функцией на смешанном пространстве.

LaTeX

$$$ \forall w,\; \operatorname{Continuous}(\operatorname{normAtPlace}(w)) $$$

Lean4

@[fun_prop]
theorem continuous_normAtPlace (w : InfinitePlace K) : Continuous (normAtPlace w) :=
  by
  simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
  split_ifs <;> fun_prop

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