Revision #1348 → #2461 · back to history
modifiedLattice in real coordinate space3fc16b995b77
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | IsZLattice |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Basic |
| note | — | IsZLattice K L characterizes a discrete Z-submodule whose K-span is the ambient space, generalizing the R^n definition. |
| status | — | formalized |
modifiedSquare lattice and integer latticesa48f77e93f99
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | instIsZLatticeRealSpan |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Basic |
| note | — | The Z-span of the standard basis in ι → ℝ is an IsZLattice instance, giving the integer lattice; no named `squareLattice` decl exists. |
| status | — | partial |
modifiedLattice is a Delone setc218652f9b19
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | Delone.DeloneSet |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.AperiodicOrder.Delone.Basic |
| note | — | Delone sets are defined but there is no lemma exhibiting a ℤ-lattice as a Delone set. |
| status | — | partial |
modifiedLattice as free abelian group spanning vector space4e96c2662c3d
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | ZLattice.module_free |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Basic |
| note | — | ZLattice.module_free states that any IsZLattice is a free ℤ-module, complementing IsZLattice.span_top for the spanning condition. |
| status | — | formalized |
modifiedLattice as symmetry group of discrete translational symmetryb84c555bea75
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no notion of a translation-symmetry group of a subset of Euclidean space, so this characterization is not formalized. |
| status | — | not_formalized |
addedLattice is a finitely generated free abelian group3cfb724be83d
modifiedE8 and Leech latticesa232f44206c4
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Grep for E8/Leech turns up only ADE-inequality/root-system material, with no lattice construction. |
| status | — | not_formalized |
addedChange of basis by integer transition matrixec87d7e82d96
modifiedFundamental domain / primitive cell8b2751337da8
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | ZSpan.fundamentalDomain |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Basic |
| note | — | ZSpan.fundamentalDomain builds the parallelepiped for a basis and ZSpan.isAddFundamentalDomain shows it is a fundamental domain of the lattice action. |
| status | — | formalized |
modifiedCovolume and unimodular lattice00ee01218d0c
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | ZLattice.covolume |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Covolume |
| note | — | ZLattice.covolume defines the covolume; there is no `Unimodular` predicate for lattices in Mathlib. |
| status | — | partial |
modifiedMinkowski's theorem4010b777b32b
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.MeasureTheory.Group.GeometryOfNumbers |
| note | — | This file states the Minkowski Convex Body Theorem in both strict and compact-domain forms. |
| status | — | formalized |
addedEhrhart polynomial of a lattice polytopea7b6ee82cb33
addedLLL lattice basis reduction algorithma11ecc70ee6d
modifiedCrystallographic restriction (five 2D lattice types)a1ea5069d2a9
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | IsCrystallographic exists only for root pairings; the 2D classification into five Bravais types is not present. |
| status | — | not_formalized |
modifiedPeriod lattice and basis in 2Dbf8df3aa1df9
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | PeriodPair.lattice |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass |
| note | — | PeriodPair.lattice defines the ℤ-submodule of ℂ generated by two periods ω₁, ω₂. |
| status | — | formalized |
modifiedFundamental parallelogram in 2De73dcc5e863a
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | ZSpan.fundamentalDomain |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Basic |
| note | — | The general fundamental parallelepiped and its basis-independent volume via ZLattice.covolume_eq_det specialize to the 2D area-by-cross-product fact, but the 2D statement is not called out separately. |
| status | — | partial |
modifiedComplex representation and modular group action7be67ca874e6
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | ModularGroup |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.NumberTheory.Modular |
| note | — | SL(2,ℤ) and its action on the upper half-plane are formalized, but no statement identifies its orbits with equivalence classes of 2D lattices. |
| status | — | partial |
modified14 Bravais lattices in 3D0f61882c0031
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Bravais lattices are not in Mathlib. |
| status | — | not_formalized |
modifiedLattice in complex space50f4d177158b
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | IsZLattice |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.Module.ZLattice.Basic |
| note | — | IsZLattice K L applies with K = ℝ and E = ℂ^n, capturing a discrete Z-submodule whose ℝ-span (dim 2n) is the whole space. |
| status | — | formalized |
addedRank of a lattice in complex n-space3c4a7ec31428
modifiedGaussian integers as a latticeecb09fe875f4
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | GaussianInt |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.NumberTheory.Zsqrtd.GaussianInt |
| note | — | GaussianInt = ℤ[i] is defined as a ring, but there is no explicit IsZLattice instance exhibiting its image in ℂ as a lattice. |
| status | — | partial |
modifiedLattice in a Lie group3b9d2e7d458a
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No general Lie-group lattice notion (discrete subgroup with finite Haar-covolume quotient) is defined in Mathlib. |
| status | — | not_formalized |
modifiedUniform / cocompact latticedf43218f2f85
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The concept of a cocompact/uniform lattice in a Lie group is not defined in Mathlib. |
| status | — | not_formalized |
modifiedR-lattice in a vector spacece7c81e6ab7b
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | Submodule.IsLattice |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Module.Lattice |
| note | — | Submodule.IsLattice A M asserts that an R-submodule M of a K-vector space is finitely generated with K-span equal to the whole space. |
| status | — | formalized |
modifiedLattices generated by GL-related bases are isomorphic876ecd69b511
| Field | From #1348 | To #2461 |
|---|
| anchor.snippet | different bases B will generate different lattices | then the lattices generated by these bases will be isomorphic |
| label | Isomorphism of lattices under GL transition matrix | Lattices generated by GL-related bases are isomorphic |
| mathlib.decl | — | Module.Basis.isUnit_det |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.Determinant |
| note | — | General basis-change-is-unit results specialize to give the equivalence of lattices related by an invertible R-matrix, but no dedicated lemma is stated for R-lattices. |
| provenance | ai-agent1 | ai-moderated |
| status | — | partial |
modifiedDual lattice in inner product spacebc8991465cf6
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | LinearMap.BilinForm.dualSubmodule |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.LinearAlgebra.BilinearForm.DualLattice |
| note | — | The dual submodule with respect to a bilinear form is defined generally; applied to the inner-product form on a lattice this gives the dual lattice. |
| status | — | partial |
modifiedPrimitive element of a latticeb0d0ed3223be
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `primitive element of a lattice` notion (indivisible vector in a ℤ-lattice) is present in Mathlib. |
| status | — | not_formalized |
modifiedPrimitive generator of one-dimensional sublatticeeb1ddce503a6
| Field | From #1348 | To #2461 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The statement that every rank-one sublattice is generated by a primitive vector is not present. |
| status | — | not_formalized |
modifiedSaturated sublattice (equivalent conditions)a646ae0f8f5e
| Field | From #1348 | To #2461 |
|---|
| anchor.snippet | We say | is a saturated sublattice whenever any of the following equivalent conditions holds |
| mathlib.decl | — | AddSubmonoid.NSMulSaturated |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.GroupTheory.Subgroup.Saturated |
| note | — | The abstract saturated-subgroup notion (n·g ∈ H ⇒ n=0 ∨ g ∈ H) generalizes saturation for sublattices, but the multiple equivalent conditions bundle is not spelled out. |
| provenance | ai-agent1 | ai-moderated |
| status | — | partial |