Xavier Roblot

After a quick search online, it would appear that the answer is [no](https://math.stackexchange.com/questions/1996480/every-totally-ordered-field-satisfying-archimedean-property-can-be-embedded-in-t)

Here is a new version with a lemma: ```lean variables {R S : Type*} [linear_ordered_field R] [linear_ordered_field S] lemma ring_hom_monotone (hR : ∀ r : R, 0 ≤ r →...

I have committed a new proof of Minkowski's theorem (and Blichfeldt's theorem) that doesn't require a basis and thus doesn't rely anymore on #18343

~~The new version requires the hypothesis `measurable_set T`. As suggested by @YaelDillies, it would be nice to remove this hypothesis using the fact that `T` is convex using [convex.null_measurable_set](https://leanprover-community.github.io/mathlib_docs/analysis/convex/measure.html#convex.null_measurable_set).~~ ~~But,...

bors r+

bors r+

It would be nice if you could also add the equivalent of [MeasureTheory.ContinuousOn.hasBoxIntegral](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/BoxIntegral/Integrability.html#MeasureTheory.ContinuousOn.hasBoxIntegral) for this case.

Could you merge with Mathlib to resolve the conflict? I was busy grading copies lately but I should be able to have another look at this PR today or tomorrow

I am not at all in expert in this domain so I cannot really comment on the math. The code we wrote is really good but sometimes a little less...

> I wouldn't really consider myself an expert in the area either, but I doubt that there's going to be a substantially easier way to prove this. > > I...