Theorems · Definition · commutative algebra

Algebra.intNorm

(A : Type u_1) →
  (B : Type u_6) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [IsIntegrallyClosed A] →
            [IsDomain A] →
              [IsDomain B] → [IsIntegrallyClosed B] → [Algebra.IsIntegral A B] → [Module.IsTorsionFree A B] → B →* A

The norm of a finite extension of integrally closed domains B/A is the restriction of the norm on Frac(B)/Frac(A) onto B/A. See Algebra.algebraMap_intNorm.

Defined in

Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Cited by

28 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsIntegrallyClosedIsDomainIsDomainIsIntegrallyClosedAlgebra.IsIntegralModule.IsTorsionFree