OAI/Geometry/PeriodicTiling/LatticePeriodicity.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PeriodicTilingThree.scaledCoordinateBasisline 13 - theorem
OAI.PeriodicTilingThree.scaledCoordinateBasis_eq_castline 16 - theorem
OAI.PeriodicTilingThree.exists_positive_scalar_sublatticeline 27 - theorem
OAI.PeriodicTilingThree.FullyPeriodic.castLattice_imageline 33