Theorems · Definition · logic and foundations
HahnSeries.cardSuppLTAddSubmonoid
(Γ : Type u_1) →
(R : Type u_2) →
(κ : Cardinal.{u_1}) →
[inst : PartialOrder Γ] →
[inst_1 : AddMonoid R] → [hκ : Fact (Cardinal.aleph0 ≤ κ)] → AddSubmonoid (HahnSeries Γ R)The κ-bounded submonoid of Hahn series with less than κ terms.
- Defined in
- Mathlib.RingTheory.HahnSeries.Cardinal
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrderAddMonoidFact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Set.ofPredproof · cited by 6,101
- AddMonoidstatement and proof · cited by 2,864
- Factstatement and proof · cited by 2,726
- Cardinalstatement and proof · cited by 2,598
- AddSubmonoidstatement · cited by 1,178
- HahnSeriesstatement and proof · cited by 528
- Cardinal.aleph0statement and proof · cited by 521
- HahnSeries.cardSuppproof · cited by 28
Cited by4
Results whose statement or proof uses this declaration.
- HahnSeries.cardSuppLTAddSubgroupproof · cited by 4
- HahnSeries.cardSuppLTAddSubmonoid.congr_simpstatement and proof · cited by 0
- HahnSeries.mem_cardSuppLTAddSubmonoidstatement · cited by 0
- HahnSeries.coe_cardSuppLTAddSubmonoidstatement and proof · cited by 0