Theorems · Definition · commutative algebra
HahnSeries.C
{Γ : Type u_1} →
{R : Type u_3} →
[inst : AddCommMonoid Γ] →
[inst_1 : PartialOrder Γ] →
[inst_2 : IsOrderedCancelAddMonoid Γ] → [inst_3 : NonAssocSemiring R] → R →+* HahnSeries Γ RC a is the constant Hahn Series a. C is provided as a ring homomorphism.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- RingHomstatement · cited by 10,189
- PartialOrderstatement and proof · cited by 6,410
- NonAssocSemiringstatement and proof · cited by 805
- HahnSeriesstatement · cited by 528
- IsOrderedCancelAddMonoidstatement and proof · cited by 359
- HahnSeries.singleproof · cited by 82
Cited by15
Results whose statement or proof uses this declaration.
- HahnSeries.C_applystatement and proof · cited by 6
- HahnSeries.ofPowerSeries_Cstatement · cited by 3
- HahnSeries.C_zerostatement and proof · cited by 2
- HahnSeries.C_injectivestatement and proof · cited by 1
- HahnSeries.C_onestatement and proof · cited by 1
- HahnSeries.C_mul_eq_smulstatement · cited by 0
- HahnSeries.C_ne_zerostatement · cited by 0
- LaurentSeries.algebraMap_C_mem_adicCompletionIntegersstatement and proof · cited by 0
- LaurentSeries.algebraMap_applystatement · cited by 0
- HahnSeries.algebraMap_applystatement · cited by 0
- PowerSeries.coe_Cstatement · cited by 0
- HahnSeries.map_Cstatement and proof · cited by 0