English
Let A be finite free over S, S over R, with R,S commutative. Then the norm from A to R equals the composition of the two intermediate norms: Norm_{A/R} = Norm_{S/R} ∘ Norm_{A/S}.
Русский
Пусть A над R и S образует тензорную цепочку, где A — конечномерная свободная над S, и S над R. Тогда нормa от A к R равна композиции норм от A к S и норм от S к R.
LaTeX
$$$\\mathrm{Norm}_{A/R} = \\mathrm{Norm}_{S/R} \\circ \\mathrm{Norm}_{A/S}.$$$
Lean4
/-- Let A/S/R be a tower of finite free tower of rings (with R and S commutative).
Then $\text{Norm}_{A/R} = \text{Norm}_{A/S} \circ \text{Norm}_{S/R}$. -/
theorem norm_norm {A} [Ring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Module.Free S A] {a : A} :
norm R (norm S a) = norm R a := by rw [norm_apply S, norm_apply R a, ← LinearMap.det_restrictScalars]; rfl
