Theorems · Definition · commutative algebra

Ideal.spanNorm

(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] → Ideal S → Ideal R

Ideal.spanNorm R (I : Ideal S) is the ideal generated by mapping Algebra.intNorm R S over I. See also Ideal.relNorm.

Defined in

Mathlib.RingTheory.Ideal.Norm.RelNorm

Cited by

19 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainIsIntegrallyClosedIsIntegrallyClosedAlgebraModule.FiniteModule.IsTorsionFree