Theorems · Definition · commutative algebra
FractionalIdeal.spanSingleton
{R : Type u_5} →
[inst : CommRing R] →
(S : Submonoid R) →
{P : Type u_6} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → [IsLocalization S P] → P → FractionalIdeal S PspanSingleton x is the fractional ideal generated by x if 0 ∉ S
- Cited by
- 73 results in Mathlib
- Foundations
- Depth 31 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.
- CommRingstatement · cited by 17,173
- Algebrastatement · cited by 11,388
- Submonoidstatement · cited by 3,086
- IsLocalizationstatement · cited by 636
- FractionalIdealstatement · cited by 423
Cited by73
Results whose statement or proof uses this declaration.
- FractionalIdeal.spanSingleton_onestatement · cited by 12
- FractionalIdeal.coe_spanSingletonstatement · cited by 11
- FractionalIdeal.spanSingleton_mul_spanSingletonstatement and proof · cited by 11
- FractionalIdeal.spanSingleton_zerostatement · cited by 11
- FractionalIdeal.coeIdeal_span_singletonstatement · cited by 10
- FractionalIdeal.spanSingleton.congr_simpstatement and proof · cited by 8
- FractionalIdeal.exists_eq_spanSingleton_mulstatement and proof · cited by 6
- FractionalIdeal.mem_spanSingletonstatement · cited by 6
- FractionalIdeal.count_well_definedstatement and proof · cited by 5
- FractionalIdeal.den_mul_self_eq_num'statement and proof · cited by 5
- FractionalIdeal.ideal_factor_ne_zerostatement and proof · cited by 4
- FractionalIdeal.mem_spanSingleton_selfstatement · cited by 4