Zulip Chat Archive

Stream: general

Topic: order of inputs to function


Kevin Buzzard (Nov 14 2018 at 13:48):

Sorry if this is already covered somewhere. What should the order of the inputs be in a definition such as

lemma nth_root_pow_left {x : } {m n : } (Hm : 0 < m) (Hx : 0 < x) :
(nth_root x m) ^ (m * n) = x ^ n :=

? I'm writing a little library about n'th roots and I've realised that I'm just putting the reals and nats and positivity facts in random and inconsistent orders.

Kenny Lau (Nov 14 2018 at 13:53):

x before m, so x before m


Last updated: Dec 20 2023 at 11:08 UTC