Theorems · Definition · commutative algebra
LocalizedModule.Away
{R : Type u_1} →
[inst : CommSemiring R] → R → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)Given x : R, LocalizedModule.Away x M is the localization of M at the
submonoid generated by x.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Modulestatement and proof · cited by 20,661
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- Submonoid.powersproof · cited by 408
- LocalizedModuleproof · cited by 154
Cited by20
Results whose statement or proof uses this declaration.
- LocalizedModule.subsingleton_iff_support_subsetstatement · cited by 5
- exists_bijective_map_powersproof · cited by 3
- Algebra.basicOpen_subset_etaleLocus_iffproof · cited by 3
- Algebra.basicOpen_subset_smoothLocus_iffproof · cited by 3
- Algebra.basicOpen_subset_unramifiedLocus_iffproof · cited by 3
- Module.FinitePresentation.exists_free_localizedModule_powersstatement and proof · cited by 2
- LocalizedModule.exists_subsingleton_awaystatement · cited by 2
- Module.basicOpen_subset_freeLocus_iffstatement · cited by 2
- Module.FinitePresentation.exists_basis_localizedModule_powersstatement and proof · cited by 1
- Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModulestatement · cited by 1
- Module.isLocallyConstant_rankAtStalk_freeLocusproof · cited by 1
- Module.isOpen_freeLocusproof · cited by 1