Theorems · Theorem · commutative algebra

RingHom.RespectsIso.cancel_right_isIso

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [CategoryTheory.IsIso g],
      P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) ↔ P (CommRingCat.Hom.hom f)

Defined in

Mathlib.RingTheory.RingHomProperties

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.IsIso