Theorem NumberField.mixedEmbedding.latticeBasis_apply

Modification history

2024-02-07 19:45

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

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

Modified NumberField.mixedEmbedding.latticeBasis_apply View on Github →

2023-09-20 09:38

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt (#5650) …

Added NumberField.mixedEmbedding.latticeBasis_apply View on Github →