Theorems · Theorem · commutative algebra

FractionalIdeal.ringEquivOfRingEquiv_trans_apply

∀ {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] {T : Type u_9}
  [inst_10 : CommRing T] [inst_11 : IsDomain T] (M : Type u_10) [inst_12 : CommRing M] [inst_13 : Algebra T M]
  [inst_14 : IsFractionRing T M] (f : R ≃+* S) (g : S ≃+* T) (I : FractionalIdeal (nonZeroDivisors R) K),
  (FractionalIdeal.ringEquivOfRingEquiv K M (f.trans g)) I =
    (FractionalIdeal.ringEquivOfRingEquiv L M g) ((FractionalIdeal.ringEquivOfRingEquiv K L f) I)

Defined in

Mathlib.RingTheory.FractionalIdeal.Operations

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainCommRingCommRingAlgebraAlgebraIsFractionRingIsFractionRingCommRingIsDomainCommRingAlgebraIsFractionRing