Theorems · Theorem · number theory
NumberField.InfinitePlace.norm_embedding_eq
∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : K), ‖w.embedding x‖ = w x- Cited by
- 10 results in Mathlib
- Foundations
- Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- RingHomstatement · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Complexstatement · cited by 5,565
- Norm.normstatement and proof · cited by 5,413
- NumberField.InfinitePlacestatement and proof · cited by 604
- NumberField.InfinitePlace.embeddingstatement and proof · cited by 78
- NumberField.InfinitePlace.mk_embeddingproof · cited by 25
Cited by10
Results whose statement or proof uses this declaration.
- NumberField.mixedEmbedding.normAtPlace_applyproof · cited by 8
- NumberField.is_primitive_element_of_infinitePlace_ltproof · cited by 3
- NumberField.InfinitePlace.norm_embedding_of_isRealproof · cited by 2
- NumberField.InfinitePlace.isometry_embeddingproof · cited by 2
- NumberField.finite_setOfPred_prod_infinitePlace_iSup_leproof · cited by 2
- NumberField.mixedEmbedding.convexBodyLT'_memproof · cited by 1
- NumberField.mixedEmbedding.convexBodyLT_memproof · cited by 1
- NumberField.exists_conjugate_one_le_normproof · cited by 1
- NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplexproof · cited by 1
- NumberField.IsCMField.infinitePlace_complexConjproof · cited by 0