Theorem NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal

Modification history

2024-04-05 07:05

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

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

Modified NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal View on Github →

2024-02-23 11:29

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

feat: Proof of Hermite theorem on number fields of bounded discriminant (#10030) …

Added NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal View on Github →