Theorems · Theorem · commutative algebra
HahnSeries.coeff_single_same
∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (a : Γ) (r : R),
((HahnSeries.single a) r).coeff a = r- Defined in
- Mathlib.RingTheory.HahnSeries.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrderZero
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.
- DFunLike.coestatement · cited by 62,936
- PartialOrderstatement and proof · cited by 6,410
- HahnSeriesstatement · cited by 528
- HahnSeries.coeffstatement · cited by 235
- ZeroHomstatement · cited by 161
- Pi.single_eq_sameproof · cited by 144
- HahnSeries.singlestatement · cited by 82
Cited by14
Results whose statement or proof uses this declaration.
- HahnSeries.single_mul_singleproof · cited by 6
- HahnSeries.coeff_singleproof · cited by 4
- HahnSeries.coeff_mul_single_addproof · cited by 3
- HahnSeries.embDomain_singleproof · cited by 2
- HahnSeries.leadingCoeff_of_singleproof · cited by 2
- HahnSeries.single_injectiveproof · cited by 2
- HahnModule.coeff_single_smul_vaddproof · cited by 2
- HahnSeries.C_injectiveproof · cited by 1
- HahnEmbedding.Partial.apply_of_mem_stratumproof · cited by 1
- LaurentSeries.hasseDeriv_single_addproof · cited by 1
- HahnSeries.map_singleproof · cited by 1
- HahnSeries.coeff_order_of_eq_add_singleproof · cited by 1