Theorems · Definition · commutative algebra

RingHom.OfLocalizationSpanTarget

({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop

A property P of ring homs satisfies RingHom.OfLocalizationSpanTarget if P holds for R →+* S whenever there exists a set { r } that spans S such that P holds for R →+* Sᵣ. Note that this is equivalent to RingHom.OfLocalizationFiniteSpanTarget via RingHom.ofLocalizationSpanTarget_iff_finite, but this has less restrictions when applying.

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

14 results in Mathlib

Foundations

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