Theorems · Theorem · commutative algebra

HomogeneousLocalization.Away.eventually_smul_mem

∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ} [GradedRing 𝒜] {f : A}
  {m : ι},
  f ∈ 𝒜 m →
    ∀ (z : HomogeneousLocalization.Away 𝒜 f),
      ∀ᶠ (n : ℕ) in Filter.atTop,
        f ^ n • HomogeneousLocalization.val z ∈ ⇑(algebraMap A (Localization (Submonoid.powers f))) '' ↑(𝒜 (n • m))

Defined in

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeAddSubgroupClassAddCommMonoidDecidableEqGradedRing