Can't find a theorem that works

Stream: Is there code for X?

[Timothy Harevy]

Want to rewrite the following

(↑n)⁻¹ < ε

as

1<(↑n)*ε

Epsilon is in the Reals and n in the natural numbers tried using inv_lt_iff_one_lt_mul which is defined as

theorem inv_lt_iff_one_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
a⁻¹ < b ↔ 1 < b * a

but this doesn't work I'm not sure what I'm missing

[Damiano Testa]

The lemma that you mention applies to a Group (under multiplication), which the reals are not. The lemma docs#div_lt_iff is close to what might be able to use, but it applies to a / b, rather than x⁻¹.

[Damiano Testa]

If the form of inv_lt_iff does not really exist, then it might also be a lemma that could be added to Mathlib.

[Timothy Harevy]

thank you might give it a go then

[Kevin Buzzard]

Note that the rewrite is impossible in general because n=0 satisfies the first equation but not the second (at least I think it does, android is not displaying the first equation correctly for me because of a known bug, the point is that 1/0=0 in lean)

[Floris van Doorn]

Is this docs#inv_pos_lt_iff_one_lt_mul (or docs#inv_pos_lt_iff_one_lt_mul')?