English
If L/K is Galois, the algebra map of intNorm equals the product over all K-automorphisms of L of the images of x, i.e., the norm equals the product of conjugates.
Русский
Если расширение L/K Gî, то алгебраическое отображение intNorm равно произведению по всем K-автоморфизмам L от образов x, то есть норма равна произведению сопряжённых элементов.
LaTeX
$$$[IsGalois (FractionRing A) (FractionRing B)]\\{x:\\, B} : algebraMap A B (intNorm A B x) = \\prod_{\\sigma \\in B \\simeq_A B} σ x$$$
Lean4
theorem intNorm_intNorm {C : Type*} [CommRing C] [IsDomain C] [IsIntegrallyClosed C] [Algebra A C] [Algebra B C]
[IsScalarTower A B C] [Module.Finite A C] [Module.Finite B C] [NoZeroSMulDivisors A C] [NoZeroSMulDivisors B C]
(x : C) : intNorm A B (intNorm B C x) = intNorm A C x :=
by
apply FaithfulSMul.algebraMap_injective A (FractionRing A)
rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing,
Algebra.norm_norm]
