Commit 2025-10-09 12:15 6a1dc6b6

View on Github →

feat(GroupTheory): add DivisibleHull (#29275) This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of LocalizedModule that this PR uses. Hopefully I avoided interfering it by using mostly with public API.

Estimated changes

deleted theorem le_of_pow_le_pow_left'
added theorem pow_le_pow_iff_left
modified theorem NNRat.divNat_zero
added theorem NNRat.mk_zero
added theorem DivisibleHull.coe_add
added theorem DivisibleHull.coe_inj
added theorem DivisibleHull.ind
added def DivisibleHull.mk
added theorem DivisibleHull.mk_eq_mk
added theorem DivisibleHull.mk_le_mk
added theorem DivisibleHull.mk_lt_mk
added theorem DivisibleHull.mk_zero
added theorem DivisibleHull.neg_mk
added theorem DivisibleHull.nsmul_mk
added theorem DivisibleHull.qsmul_mk
added theorem DivisibleHull.zsmul_mk