Theorems · Theorem · commutative algebra

RingHom.locally_StableUnderCompositionWithLocalizationAwaySource

Deprecated since 2026-02-11Use RingHom.locally_stableUnderCompositionWithLocalizationAwaySource instead.

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P

Alias of RingHom.locally_stableUnderCompositionWithLocalizationAwaySource. If P is stable under composition with localization away maps on the left, then so is Locally P.

Defined in: Mathlib.RingTheory.RingHom.Locally
Cited by: 0 results in Mathlib
Foundations: Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement · cited by 17,173
RingHomstatement · cited by 10,189
RingHom.Locallystatement · cited by 28
RingHom.StableUnderCompositionWithLocalizationAwaySourcestatement · cited by 6
RingHom.locally_stableUnderCompositionWithLocalizationAwaySourceproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.