English
The norm from K is compatible with nesting of towers under finite dimensionality and IsScalarTower; i.e., norm_K(x) behaves compatibly with norm_F and the canonical identifications.
Русский
Нормa от K совместима с вложениями в башне полей при конечном размерности и условии IsScalarTower; нормa_K ведет себя совместимо с norm_F и каноническими идентификациями.
LaTeX
$$$[\text{Algebra } F L] \land [\text{FiniteDimensional } F L] \land [\text{IsScalarTower } K F L] (x : \mathscr{O}L) : \operatorname{norm}_K(\operatorname{norm}_F x) = \operatorname{norm}_K x$$$
Lean4
theorem norm_norm [Algebra F L] [FiniteDimensional F L] [IsScalarTower K F L] (x : 𝓞 L) :
norm K (norm F x) = norm K x := by rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]
