Theorems · Theorem · commutative algebra

FractionalIdeal.ringEquivOfRingEquiv_trans

∀ {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),
  FractionalIdeal.ringEquivOfRingEquiv K M (f.trans g) =
    (FractionalIdeal.ringEquivOfRingEquiv K L f).trans (FractionalIdeal.ringEquivOfRingEquiv L M g)

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

CommRingIsDomainCommRingIsDomainCommRingCommRingAlgebraAlgebraIsFractionRingIsFractionRingCommRingIsDomainCommRingAlgebraIsFractionRing