Theorems · Definition · commutative algebra

RingHom.OfLocalizationFiniteSpan

({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 finite set { r } that spans R such that P holds for Rᵣ →+* Sᵣ. Note that this is equivalent to RingHom.OfLocalizationSpan via RingHom.ofLocalizationSpan_iff_finite, but this is easier to prove.

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

1 results in Mathlib

Foundations

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