Theorems · Theorem · commutative algebra

RingHom.IsStableUnderBaseChange.mk

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    (∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
        [inst_4 : Algebra R T], P (algebraMap R T) → P (algebraMap S (TensorProduct R S T))) →
      RingHom.IsStableUnderBaseChange P

Defined in

Mathlib.RingTheory.RingHomProperties

Cited by

16 results in Mathlib

Foundations

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