Theorems · Theorem · commutative algebra

FractionalIdeal.ringEquivOfRingEquiv_spanSingleton

∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S) (x : K),
  (FractionalIdeal.ringEquivOfRingEquiv K L f) (FractionalIdeal.spanSingleton (nonZeroDivisors R) x) =
    FractionalIdeal.spanSingleton (nonZeroDivisors S) ((IsFractionRing.ringEquivOfRingEquiv f) x)

Defined in

Mathlib.RingTheory.FractionalIdeal.Operations

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainCommRingCommRingAlgebraAlgebraIsFractionRingIsFractionRing