Theorems · Inductive type · commutative algebra

RingHom.PropertyIsLocal

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

A property of ring homs is local if it is preserved by localizations and compositions, and for each { r } that spans S, we have P (R →+* S) ↔ ∀ r, P (R →+* Sᵣ).

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

20 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms