English
If A and B satisfy separability and integrality hypotheses, then x divides algebraMap_A_B(intNorm_A_B x) in B, i.e., x | algebraMap_A B (intNorm x).
Русский
При удовлетворяющих условиям разделимости и интегрирования, элемент x делит algebraMap_A_B(intNorm_A_B x) в B.
LaTeX
$$$[Algebra.IsSeparable (FractionRing A) (FractionRing B)] (x : B) : x \\mid algebraMap A B (intNorm A B x)$$$
Lean4
@[simp]
theorem intNorm_map_algEquiv [IsDomain B₂] [IsIntegrallyClosed B₂] [Module.Finite A B₂] [NoZeroSMulDivisors A B₂]
(x : B) (σ : B ≃ₐ[A] B₂) : Algebra.intNorm A B₂ (σ x) = Algebra.intNorm A B x :=
by
apply FaithfulSMul.algebraMap_injective A (FractionRing A)
rw [algebraMap_intNorm_fractionRing, algebraMap_intNorm_fractionRing, ←
galLiftEquiv_algebraMap_apply (FractionRing A) (FractionRing B), norm_eq_of_algEquiv]
