Theorems · Definition · number theory
NumberField.InfinitePlace.IsReal
{K : Type u_1} → [inst : Field K] → NumberField.InfinitePlace K → PropAn infinite place is real if it is defined by a real embedding.
- Cited by
- 301 results in Mathlib
- Foundations
- Depth 139 from the axioms, rests on 3,711 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
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.
- RingHomproof · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Complexproof · cited by 5,565
- NumberField.InfinitePlacestatement and proof · cited by 604
- NumberField.InfinitePlace.mkproof · cited by 56
- NumberField.ComplexEmbedding.IsRealproof · cited by 38
Cited by345
Results whose statement or proof uses this declaration.
- NumberField.mixedEmbedding.mixedSpaceproof · cited by 239
- NumberField.InfinitePlace.multproof · cited by 107
- NumberField.mixedEmbeddingstatement and proof · cited by 52
- NumberField.mixedEmbedding.normstatement · cited by 46
- NumberField.mixedEmbedding.normAtPlacestatement and proof · cited by 45
- NumberField.mixedEmbedding.realMixedSpaceproof · cited by 34
- NumberField.InfinitePlace.nrRealPlacesproof · cited by 33
- NumberField.InfinitePlace.not_isReal_iff_isComplexstatement and proof · cited by 25
- NumberField.mixedEmbedding.mixedSpaceOfRealSpacestatement and proof · cited by 20
- NumberField.mixedEmbedding.negAtstatement and proof · cited by 20
- NumberField.mixedEmbedding.polarCoordstatement and proof · cited by 15
- NumberField.mixedEmbedding.indexproof · cited by 15
Showing the 200 most cited of 345.