Theorems · Theorem · number theory
NumberField.InfinitePlace.liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver
∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
{v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
w ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v →
NumberField.ComplexEmbedding.LiesOver (NumberField.ComplexEmbedding.conjugate w.embedding) v.embedding- Cited by
- 1 results in Mathlib
- Foundations
- Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- NumberField.InfinitePlacestatement and proof · cited by 604
- NumberField.InfinitePlace.embeddingstatement and proof · cited by 78
- NumberField.ComplexEmbedding.conjugatestatement · cited by 40
- NumberField.InfinitePlace.LiesOverproof · cited by 25
- NumberField.ComplexEmbedding.LiesOverstatement · cited by 19
- NumberField.InfinitePlace.ramifiedPlacesOverstatement and proof · cited by 12
- NumberField.InfinitePlace.LiesOver.comap_eqproof · cited by 9
- NumberField.InfinitePlace.IsRamified.comap_embedding_conjugateproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- NumberField.InfinitePlace.conjugate_embedding_mem_mixedEmbeddingsOverproof · cited by 1