Theorems · Theorem · commutative algebra

RingHom.locally_of_locally

∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f) →
    ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
      RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f →
        RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => Q) f

Defined in

Mathlib.RingTheory.RingHom.Locally

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRing