Theorems · Definition · commutative algebra

RingHom.OfLocalizationSpan

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

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

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

16 results in Mathlib

Foundations

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