Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-24 18:18 271bf175

View on Github →

feat(number_theory/number_field/embeddings): some additional lemmas (#18473) Add some small lemmas that will be useful for other PRs.

Estimated changes

Modified src/number_theory/number_field/embeddings.lean

added theorem number_field.infinite_place.abs_embedding

added theorem number_field.infinite_place.eq_iff_eq

added theorem number_field.infinite_place.le_iff_le

modified theorem number_field.infinite_place.mk_complex.apply

added theorem number_field.infinite_place.mk_complex_coe

added theorem number_field.infinite_place.mk_complex_embedding

modified theorem number_field.infinite_place.mk_real.apply

added theorem number_field.infinite_place.mk_real_coe

modified theorem number_field.infinite_place.pos_iff