Theorems · Theorem · commutative algebra

RingHom.Locally.span_eq_top

∀ (P : {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},
  RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f →
    Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)} = ⊤

Alias of the forward direction of RingHom.locally_iff_span_eq_top.

Defined in

Mathlib.RingTheory.RingHom.Locally

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRing