Theorems · Theorem · field theory
ConditionallyCompleteLinearOrderedField.inducedMap_self
∀ {β : Type u_3} [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] (b : β),
ConditionallyCompleteLinearOrderedField.inducedMap β β b = b- Defined in
- Mathlib.Algebra.Order.CompleteField
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- IsStrictOrderedRingstatement and proof · cited by 2,490
- ConditionallyCompleteLinearOrderstatement and proof · cited by 542
- ConditionallyCompleteLinearOrderedField.inducedMapstatement · cited by 28
- ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iffproof · cited by 4
- eq_of_forall_rat_lt_iff_ltproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- ConditionallyCompleteLinearOrderedField.inducedMap_inv_selfproof · cited by 1
- ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_selfproof · cited by 1
- LinearOrderedField.inducedMap_selfproof · cited by 0