Theorems · Theorem · order theory
HahnEmbedding.Partial.eval_zero
∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
{M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
[inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
[inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
[inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R], f.eval 0 = 0- Cited by
- 2 results in Mathlib
- Foundations
- Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Top.topstatement and proof · cited by 9,680
- LinearOrderstatement and proof · cited by 8,572
- Equivproof · cited by 8,337
- PartialOrderproof · cited by 6,410
- IsOrderedAddMonoidstatement and proof · cited by 1,659
- DivisionRingstatement and proof · cited by 1,062
- sub_selfproof · cited by 996
- IsOrderedRingstatement and proof · cited by 777
- Function.supportproof · cited by 610
Cited by2
Results whose statement or proof uses this declaration.
- HahnEmbedding.Partial.extendFun_strictMonoproof · cited by 1
- HahnEmbedding.Partial.eval_smulproof · cited by 1