Commit 2023-06-23 12:47 93488a7d

View on Github →

feat: port NumberTheory.NumberField.CanonicalEmbedding (#5414)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

added theorem NumberField.canonicalEmbedding.apply_at_complex_infinitePlace

added theorem NumberField.canonicalEmbedding.apply_at_real_infinitePlace

added def NumberField.canonicalEmbedding.equivIntegerLattice

added theorem NumberField.canonicalEmbedding.integerLattice.inter_ball_finite

added def NumberField.canonicalEmbedding.integerLattice

added theorem NumberField.canonicalEmbedding.nnnorm_eq

added theorem NumberField.canonicalEmbedding.nontrivial_space

added theorem NumberField.canonicalEmbedding.norm_le_iff

added theorem NumberField.canonicalEmbedding.space_rank

added def NumberField.canonicalEmbedding

added theorem NumberField.canonicalEmbedding_injective