powers in ordered fields

Stream: general

[Patrick Massot]

I'm trying to gather lemmas I needed for my IAS demo into a Lean PR. But I don't know where to put two lemmas. They require both linear ordered fields and group powers, neither of which imports the other.

variables {𝕜 : Type*} [linear_ordered_field 𝕜]

lemma pos_div_pow_pos {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (k : ℕ) : 0 < a/b^k :=
div_pos ha (pow_pos hb k)

lemma div_pow_le {a b : 𝕜} (ha : 0 < a) (hb : 1 ≤ b) (k : ℕ) : a/b^k ≤ a :=
(div_le_iff $ pow_pos (lt_of_lt_of_le zero_lt_one hb) k).mpr
(calc a = a *1 : by simp
   ...  ≤ a*b^k : (mul_le_mul_left ha).mpr $ one_le_pow_of_one_le hb _)

[Johan Commelin]

start a file linear_ordered_field_power?

[Patrick Massot]

This sounds a bit excessive.

[Reid Barton]

algebra.field_power?

[Patrick Massot]

I thought this was all about fpow but actually there are also gpow there.

[Patrick Massot]

Thanks.