Theorems · Definition · ring theory
Subalgebra.saturation
{R : Type u_1} →
{S : Type u_2} →
[inst : CommSemiring R] →
[inst_1 : CommSemiring S] →
[inst_2 : Algebra R S] → (s : Subalgebra R S) → (M : Submonoid S) → M ≤ s.toSubmonoid → Subalgebra R SThe saturation of a subalgebra s with respect to a submonoid M is the smallest
subalgebra closed under division by s.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Set.ofPredproof · cited by 6,101
- Submonoidstatement and proof · cited by 3,086
- Subalgebrastatement and proof · cited by 1,353
- Subsemiring.toSubmonoidstatement and proof · cited by 153
- Subalgebra.toSubsemiringstatement and proof · cited by 115
Cited by9
Results whose statement or proof uses this declaration.
- Subalgebra.saturation_saturationstatement and proof · cited by 1
- Subalgebra.le_saturationstatement · cited by 1
- Localization.localRingHom_bijective_of_saturated_inf_eq_topstatement and proof · cited by 1
- Subalgebra.mem_saturation_of_mul_mem_leftstatement and proof · cited by 1
- Algebra.ZariskisMainProperty.transstatement and proof · cited by 0
- Algebra.zariskisMainProperty_iff_exists_saturation_eq_topstatement · cited by 0
- Subalgebra.saturation.congr_simpstatement and proof · cited by 0
- Subalgebra.mem_saturation_iffstatement · cited by 0
- Subalgebra.mem_saturation_of_mul_mem_rightstatement and proof · cited by 0