Theorems · Theorem · commutative algebra

Ideal.spanNorm_singleton

∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] {r : S}, Ideal.spanNorm R (Ideal.span {r}) = Ideal.span {(Algebra.intNorm R S) r}

Defined in

Mathlib.RingTheory.Ideal.Norm.RelNorm

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainIsIntegrallyClosedIsIntegrallyClosedAlgebraModule.FiniteModule.IsTorsionFree