Zulip Chat Archive

Stream: general

Topic: powers in ordered fields


Patrick Massot (Jun 13 2020 at 17:06):

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 (Jun 13 2020 at 17:09):

start a file linear_ordered_field_power?

Patrick Massot (Jun 13 2020 at 17:17):

This sounds a bit excessive.

Reid Barton (Jun 13 2020 at 17:19):

algebra.field_power?

Patrick Massot (Jun 13 2020 at 17:21):

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

Patrick Massot (Jun 13 2020 at 17:21):

Thanks.


Last updated: Dec 20 2023 at 11:08 UTC