English
If A and B are linearly disjoint over F and one of them is algebraic, then the norm commutes with the algebra map in the appropriate way: N_A^E(a) corresponds to the algebra map of the norm from B.
Русский
Если A и B линейно разобщены над F и одно из них алгебраическое, то норма коммутирует с алгебраической картой согласованно: N_A^E(a) отображается через норму над F.
LaTeX
$$$\\operatorname{Norm}_{A}^{E}(\\iota_{B}(x)) = \\iota_{F}(\\operatorname{Norm}_{F}^{B}(x)).$$$
Lean4
/-- If `A` and `B` are linearly disjoint, then `norm` and `algebraMap` commutes.
-/
theorem norm_algebraMap [FiniteDimensional F E] (h₁ : A.LinearDisjoint B) (h₂ : A ⊔ B = ⊤) (x : B) :
Algebra.norm A (algebraMap B E x) = algebraMap F A (Algebra.norm F x) :=
by
rw [linearDisjoint_iff'] at h₁
refine h₁.norm_algebraMap ?_ x
simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg toSubalgebra h₂
