mathlib3

2aa04f65 - feat(algebra/order/to_interval_mod): lemmas about changing the base of the period (#17741)

feat(algebra/order/to_interval_mod): lemmas about changing the base of the period (#17741) The lemmas have primed names because the unprimed names refer to the versions where one of the arguments is the period.