Mathlib Map

Theorems · Definition · number theory

NumberField.ComplexEmbedding.IsReal

{K : Type u_1} → [inst : Field K] → (K →+* ℂ) → Prop

An embedding into ℂ is real if it is fixed by complex conjugation.

Defined in
Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Cited by
38 results in Mathlib
Foundations
Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Field
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NumberField.InfinitePlace.IsReal · cited by 301InfinitePlace.IsRealNumberField.InfinitePlace.IsComplex · cited by 272InfinitePlace.IsComplexNumberField.InfinitePlace.not_isReal_iff_isComplex · cited by 25InfinitePlace.not_isReal_…NumberField.InfinitePlace.isReal_iff · cited by 13InfinitePlace.isReal_iffNumberField.InfinitePlace.isReal_mk_iff · cited by 12InfinitePlace.isReal_mk_i…NumberField.InfinitePlace.card_add_two_mul_card_eq_rank · cited by 9InfinitePlace.card_add_tw…NumberField.ComplexEmbedding.isReal_iff · cited by 7ComplexEmbedding.isReal_i…NumberField.InfinitePlace.isComplex_iff · cited by 7InfinitePlace.isComplex_i…NumberField.InfinitePlace.not_isComplex_iff_isReal · cited by 5InfinitePlace.not_isCompl…NumberField.ComplexEmbedding.IsUnmixed · cited by 5ComplexEmbedding.IsUnmixedNumberField.InfinitePlace.embedding_mk_eq_of_isReal · cited by 5InfinitePlace.embedding_m…NumberField.mixedEmbedding.finrank · cited by 4mixedEmbedding.finrankNumberField.ComplexEmbedding.IsMixed · cited by 4ComplexEmbedding.IsMixedNumberField.ComplexEmbedding.isConj_one_iff · cited by 4ComplexEmbedding.isConj_o…NumberField.InfinitePlace.card_real_embeddings · cited by 3InfinitePlace.card_real_e…RingHom · cited by 10189RingHomField · cited by 7404FieldComplex · cited by 5565ComplexIsSelfAdjoint · cited by 545IsSelfAdjointComplexEmbedding.IsRealCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • RingHomstatement and proof · cited by 10,189
  • Fieldstatement and proof · cited by 7,404
  • Complexstatement and proof · cited by 5,565
  • IsSelfAdjointproof · cited by 545

Cited by45

Results whose statement or proof uses this declaration.