Theorems · Definition · commutative algebra

HomogeneousLocalization.Away

{ι : Type u_1} → {A : Type u_2} → {σ : Type u_3} → [CommRing A] → [SetLike σ A] → (ι → σ) → A → Type (max u_1 u_2)

Localizing away from powers of f homogeneously.

Defined in

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Cited by

105 results in Mathlib

Foundations

Depth 25 from the axioms, rests on 379 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingSetLike