Theorems · Definition · number theory
NumberField.mixedEmbedding.integerLattice
(K : Type u_1) → [inst : Field K] → Submodule ℤ (NumberField.mixedEmbedding.mixedSpace K)
The image of the ring of integers of K in the mixed space.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- Submodulestatement · cited by 7,192
- Complexstatement · cited by 5,565
- Algebra.algebraMapproof · cited by 4,706
- RingHom.compproof · cited by 899
- LinearMap.rangeproof · cited by 893
- NumberField.InfinitePlacestatement · cited by 604
- NumberField.RingOfIntegersproof · cited by 413
- NumberField.InfinitePlace.IsRealstatement · cited by 301
- NumberField.InfinitePlace.IsComplexstatement · cited by 272
- AlgHom.toLinearMapproof · cited by 254
Cited by7
Results whose statement or proof uses this declaration.
- NumberField.mixedEmbedding.fundamentalCone.integerSetproof · cited by 22
- NumberField.mixedEmbedding.fundamentalCone.mem_integerSetproof · cited by 4
- NumberField.mixedEmbedding.euclidean.integerLatticeproof · cited by 1
- NumberField.mixedEmbedding.span_latticeBasisstatement · cited by 1
- NumberField.mixedEmbedding.mem_span_latticeBasisstatement and proof · cited by 1
- NumberField.mixedEmbedding.fundamentalDomain_integerLatticestatement · cited by 1
- NumberField.mixedEmbedding.covolume_integerLatticestatement and proof · cited by 0