relNorm_comap_algEquiv — Mathlib

English

If σ is an algebra equivalence, relNorm_R(I.comap σ) = relNorm_R(I).

Русский

Если σ — алгебраическая эквивалентность, то relNorm_R(I.comap σ) = relNorm_R(I).

LaTeX

$$$\mathrm{relNorm}_R( I.\mathrm{comap}(\sigma) ) = \mathrm{relNorm}_R(I)$$$

Lean4

@[simp]
theorem relNorm_comap_algEquiv {T : Type*} [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T] [Algebra R T]
    [Module.Finite R T] [NoZeroSMulDivisors R T] (σ : S ≃ₐ[R] T) (I : Ideal T) : relNorm R (I.comap σ) = relNorm R I :=
  map_symm σ.toRingEquiv ▸ relNorm_map_algEquiv σ.symm I

Похожие утверждения