intNorm_idealSetEquiv_apply — Mathlib

English

Equivalences relating intNorm, absNorm, and the mixedEmbedding norm on corresponding representatives.

Русский

Эквивалентности между intNorm, absNorm и нормой смешанного вложения на соответствующих представителях.

LaTeX

$$$\\text{intNorm}(a) = \\text{absNorm}(I)$ where I corresponds to a under the equivalence.$$

Lean4

theorem intNorm_idealSetEquiv_apply (a : idealSet K J) :
    intNorm (idealSetEquiv K J a).val = mixedEmbedding.norm (a : mixedSpace K) := by
  rw [intNorm_coe, idealSetEquiv_apply]

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