Blichfeldt's Theorem

Stream: maths

[Yury G. Kudryashov]

Hi @Alex J. Best , it looks like docs#MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd is (almost?) a duplicate of docs#MeasureTheory.IsAddFundamentalDomain.exists_ne_zero_vadd_eq

[Alex J. Best]

Indeed they are pretty similar, I have no objection to merging them of course. To be honest I didn't touch the PR that much in the last year, it was the great work of @Yaël Dillies and @Xavier Roblot that got it over the line, but it probably the possibility of golfing just got overlooked as you PRed the alternate version at the same time as the minkowski pr

[Yaël Dillies]

Indeed. Feel free to move the former next to the latter and deduce one from the other.