Theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq

Modification history

2025-05-05 07:39
Mathlib/NumberTheory/NumberField/Embeddings.lean
chore(NumberField): split `embeddings.lean` (#24478) …
Modified NumberField.InfinitePlace.exists_smul_eq_of_comap_eqView on Github →
2024-08-08 10:31
Mathlib/NumberTheory/NumberField/Embeddings.lean
chore: backports for leanprover/lean4#4814 (part 36) (#15612)
Modified NumberField.InfinitePlace.exists_smul_eq_of_comap_eqView on Github →
2023-12-26 13:40
Mathlib/NumberTheory/NumberField/Embeddings.lean
feat: Define `IsUnramified` for infinite places (#9285)
Modified NumberField.InfinitePlace.exists_smul_eq_of_comap_eqView on Github →
2023-12-26 07:02
Mathlib/NumberTheory/NumberField/Embeddings.lean
feat: The galois group acts on infinite places. (#9280)
Added NumberField.InfinitePlace.exists_smul_eq_of_comap_eqView on Github →