Theorems · Inductive type · commutative algebra

HomogeneousLocalization.NumDenSameDeg

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

Let x be a submonoid of A, then NumDenSameDeg 𝒜 x is a structure with a numerator and a denominator with same grading such that the denominator is contained in x.

Defined in

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Cited by

78 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CommRingSetLike