Commit 2024-02-07 19:45 9eec23d0

View on Github →

feat: Generalize results of CanonicalEmbedding to fractional ideals (#9837) The main results of NumberTheory.NumberField.CanonicalEmbedding, that is exists_ne_zero_mem_ringOfIntegers_lt and exists_ne_zero_mem_ringOfIntegers_of_norm_le about the existence of algebraic integers satisfying special properties, are generalized from the ring of integers to fractional ideals.

Estimated changes

Modified Mathlib/Algebra/Module/Zlattice.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

added theorem NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm

added theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt

added theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le

modified theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt

added def NumberField.mixedEmbedding.fractionalIdealLatticeBasis

added theorem NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply

added def NumberField.mixedEmbedding.latticeBasis

modified theorem NumberField.mixedEmbedding.latticeBasis_apply

added theorem NumberField.mixedEmbedding.latticeBasis_repr_apply

added theorem NumberField.mixedEmbedding.mem_rat_span_latticeBasis

added theorem NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis

modified theorem NumberField.mixedEmbedding.mem_span_latticeBasis

modified theorem NumberField.mixedEmbedding.minkowskiBound_lt_top

modified theorem NumberField.mixedEmbedding.minkowskiBound_pos

added theorem NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

added theorem NumberField.abs_discr_gt_two

deleted theorem NumberField.discr_gt_one

added theorem NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr

Modified Mathlib/NumberTheory/NumberField/Units.lean