Theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le

Modification history

2024-04-05 07:05

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

chore: split `NumberTheory.NumberField.CanonicalEmbedding` (#11873) …

Modified NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le View on Github →

2024-02-07 19:45

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

feat: Generalize results of `CanonicalEmbedding` to fractional ideals (#9837) …

Added NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le View on Github →