Theorems · Definition · commutative algebra

RingHom.LocalizationPreserves

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

A property P of ring homs is said to be preserved by localization if P holds for M⁻¹R →+* M⁻¹S whenever P holds for R →+* S.

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

13 results in Mathlib

Foundations

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