Theorems · Definition · commutative algebra

Ideal.relNorm

(R : Type u_1) →
  [inst : CommRing R] →
    [IsDomain R] →
      {S : Type u_3} →
        [inst_2 : CommRing S] →
          [IsDomain S] →
            [IsIntegrallyClosed R] →
              [IsIntegrallyClosed S] →
                [inst_6 : Algebra R S] →
                  [Module.Finite R S] →
                    [Module.IsTorsionFree R S] → [IsDedekindDomain R] → [IsDedekindDomain S] → Ideal S →*₀ Ideal R

The relative norm Ideal.relNorm R (I : Ideal S), where R and S are Dedekind domains, and S is an extension of R that is finite and free as a module.

Defined in

Mathlib.RingTheory.Ideal.Norm.RelNorm

Cited by

23 results in Mathlib

Foundations

Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainCommRingIsDomainIsIntegrallyClosedIsIntegrallyClosedAlgebraModule.FiniteModule.IsTorsionFreeIsDedekindDomainIsDedekindDomain