Commit 2023-12-07 17:41 c83d3d5d

feat: add a discrete topology instance for zlattice (#8480) Add the following

variable [NormedAddCommGroup E] [NormedSpace ℝ E] (b : Basis ι ℝ E)
instance [Fintype ι] : DiscreteTopology (span ℤ (Set.range b))