Theorems · Theorem · number theory
ZLattice.module_free
∀ (K : Type u_1) [inst : NormedField K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [HasSolidNorm K] [FloorRing K]
{E : Type u_2} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace K E] [FiniteDimensional K E] [ProperSpace E]
(L : Submodule ℤ E) [inst_9 : DiscreteTopology ↥L] [IsZLattice K L], Module.Free ℤ ↥L- Defined in
- Mathlib.Algebra.Module.ZLattice.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Moduleproof · cited by 20,661
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- LinearOrderstatement and proof · cited by 8,572
- Submodulestatement and proof · cited by 7,192
- Algebra.algebraMapproof · cited by 4,706
- IsStrictOrderedRingstatement and proof · cited by 2,490
- FiniteDimensionalstatement and proof · cited by 1,854
- NormedFieldstatement and proof · cited by 1,084
- Module.Finiteproof · cited by 1,032
- Module.Freestatement · cited by 597
- FloorRingstatement and proof · cited by 405
Cited by3
Results whose statement or proof uses this declaration.
- Module.Basis.ofZLatticeBasisproof · cited by 36
- Module.Basis.ofZLatticeBasis_applyproof · cited by 11
- IsZLattice.isCompact_range_of_periodicproof · cited by 0