English
Let R be a ring and S an R-algebra with a group G acting on S by ring automorphisms in a way compatible with the R-structure. For any ideal I of S and any g ∈ G, the relative norm relNorm_R(I) is unchanged by the action: relNorm_R(g · I) = relNorm_R(I).
Русский
Пусть R — кольцо, S — алгебра R, и группа G действует на S через кольцевые автоморфизмы так, что совместимо с структурой R. Для любого идеала I в S и любого элемента g ∈ G выполняется invariance: relNorm_R(g · I) = relNorm_R(I).
LaTeX
$$$ \operatorname{relNorm}_R\bigl(g \cdot I\bigr) = \operatorname{relNorm}_R(I). $$$
Lean4
@[simp]
theorem relNorm_smul {G : Type*} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (g : G) (I : Ideal S) :
relNorm R (g • I) = relNorm R I :=
relNorm_map_algEquiv (toAlgEquiv R S g) I
