Theorems · Definition · commutative algebra

RingHom.PropertyIsLocal.casesOn

{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} →
  {motive : RingHom.PropertyIsLocal P → Sort u_1} →
    (t : RingHom.PropertyIsLocal P) →
      ((localizationAwayPreserves : RingHom.LocalizationAwayPreserves P) →
          (ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget P) →
            (ofLocalizationSpan : RingHom.OfLocalizationSpan P) →
              (StableUnderCompositionWithLocalizationAwayTarget :
                  RingHom.StableUnderCompositionWithLocalizationAwayTarget P) →
                motive ⋯) →
        motive t

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

0 results in Mathlib

Foundations

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