Theorems · Definition · commutative algebra
HomogeneousLocalization.NumDenSameDeg.deg
{ι : Type u_1} →
{A : Type u_2} →
{σ : Type u_3} →
[inst : CommRing A] →
[inst_1 : SetLike σ A] → {𝒜 : ι → σ} → {x : Submonoid A} → HomogeneousLocalization.NumDenSameDeg 𝒜 x → ι- Cited by
- 51 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Submonoidstatement and proof · cited by 3,086
- SetLikestatement and proof · cited by 1,084
- HomogeneousLocalization.NumDenSameDegstatement and proof · cited by 78
Cited by57
Results whose statement or proof uses this declaration.
- HomogeneousLocalization.NumDenSameDeg.denstatement · cited by 47
- HomogeneousLocalization.NumDenSameDeg.numstatement · cited by 42
- HomogeneousLocalization.NumDenSameDeg.den_memstatement · cited by 40
- HomogeneousLocalization.val_mkstatement · cited by 14
- AlgebraicGeometry.sectionInBasicOpenstatement and proof · cited by 6
- AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrierstatement · cited by 5
- HomogeneousLocalization.mapproof · cited by 5
- AlgebraicGeometry.mem_basicOpen_denstatement · cited by 5
- HomogeneousLocalization.NumDenSameDeg.mapproof · cited by 5
- AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eqproof · cited by 3
- AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpenstatement · cited by 2
- HomogeneousLocalization.map_compproof · cited by 2