algebraMap_norm_algebraMap — Mathlib

English

A compatibility identity relating repeated algebra maps and norms across field towers.

Русский

Свойство совместимости, связывающее повторяющиеся отображения алгебра и нормы по линейной башне полей.

LaTeX

$$$ \text{algebraMap}_{K}( \operatorname{norm}( \mathrm{algebraMap}_{\mathcal{O}K \to \mathcal{O}L} x )) = \operatorname{norm}_K ( \mathrm{algebraMap}_{K L}(x) ) $$$

Lean4

theorem algebraMap_norm_algebraMap (x : 𝓞 K) :
    algebraMap _ K (norm K (algebraMap (𝓞 K) (𝓞 L) x)) = Algebra.norm K (algebraMap K L (algebraMap _ _ x)) :=
  rfl

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