Theorems · Definition · field theory
ArchimedeanClass.FiniteElement
(K : Type u_1) → [inst : LinearOrder K] → [inst_1 : Field K] → [IsOrderedRing K] → Type u_1
The valuation subring of elements in non-negative Archimedean classes, i.e. elements bounded by some natural number.
- Defined in
- Mathlib.Algebra.Order.Ring.StandardPart
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
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.coeproof · cited by 62,936
- LinearOrderstatement and proof · cited by 8,572
- Fieldstatement and proof · cited by 7,404
- IsOrderedRingstatement and proof · cited by 777
- Valuation.valuationSubringproof · cited by 56
- AddValuation.toValuationproof · cited by 21
- ArchimedeanClass.addValuationproof · cited by 15
Cited by39
Results whose statement or proof uses this declaration.
- ArchimedeanClass.FiniteElement.mkstatement · cited by 23
- ArchimedeanClass.FiniteResidueField.mkstatement and proof · cited by 22
- ArchimedeanClass.FiniteResidueFieldproof · cited by 17
- ArchimedeanClass.stdPart_negproof · cited by 5
- ArchimedeanClass.FiniteResidueField.mk_eq_zerostatement and proof · cited by 3
- ArchimedeanClass.FiniteElement.extstatement and proof · cited by 2
- ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_posstatement and proof · cited by 2
- ArchimedeanClass.stdPart_invproof · cited by 2
- ArchimedeanClass.FiniteResidueField.mk_ne_zerostatement and proof · cited by 2
- ArchimedeanClass.stdPart_of_mk_nonnegstatement · cited by 2
- ArchimedeanClass.FiniteResidueField.ofArchimedean_applystatement · cited by 2
- ArchimedeanClass.ofArchimedean_stdPartstatement and proof · cited by 1