Theorems · Definition · commutative algebra
CauSeq.Completion.Cauchy
{α : Type u_1} →
[inst : Field α] →
[inst_1 : LinearOrder α] →
[IsStrictOrderedRing α] → {β : Type u_2} → [inst_3 : Ring β] → (abv : β → α) → [IsAbsoluteValue abv] → Type u_2The Cauchy completion of a ring with absolute value.
- Defined in
- Mathlib.Algebra.Order.CauSeq.Completion
- Cited by
- 62 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- Ringstatement and proof · cited by 7,463
- Fieldstatement and proof · cited by 7,404
- IsStrictOrderedRingstatement and proof · cited by 2,490
- IsAbsoluteValuestatement and proof · cited by 160
Cited by74
Results whose statement or proof uses this declaration.
- Padicproof · cited by 151
- CauSeq.Completion.mkstatement · cited by 24
- CauSeq.Completion.ofRatstatement · cited by 15
- Real.cauchystatement · cited by 15
- CauSeq.Completion.mk_eqstatement · cited by 3
- Real.ext_cauchy_iffstatement and proof · cited by 2
- Real.ofCauchy_onestatement · cited by 2
- Real.ofCauchy_zerostatement · cited by 2
- CauSeq.Completion.inv_mkstatement · cited by 2
- PadicSeq.ne_zero_iff_nequiv_zerostatement · cited by 2
- Real.ringEquivCauchystatement and proof · cited by 2
- Real.cauchy_negstatement and proof · cited by 1