Examples

Results named in Tau Ceti's TauCeti.Examples modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCassels' basis lemma on L#

Applied to the minima witnesses e 0, …, e 4, it gives a basis b of L with ‖b i‖ ≤ max 1 ((i + 1) / 2).

TauCeti.GaugeBasisExample.exists_basis_norm_le :
  ∃ b, ∀ (i : Fin 5), ‖↑(b i)‖ ≤ max 1 ((↑↑i + 1) / 2)

Lean

Formalized in Tau Ceti as TauCeti.GaugeBasisExample.exists_basis_norm_le.

Sources

• Tau Ceti documentation: TauCeti.GaugeBasisExample.exists_basis_norm_le
• Source of TauCeti.GaugeBasisExample.exists_basis_norm_le in TauCeti/Examples/Algebra/Module/ZLattice/GaugeBasis.lean

LeanTauCeti.GaugeBasisExample.exists_basis_norm_le

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.