Theorems · Theorem · commutative algebra

RingHom.HoldsForLocalizationAway.of_bijective

∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S)
  (P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop),
  (RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) → Function.Bijective ⇑f → P f

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRing