Zulip Chat Archive

Stream: general

Topic: abs_pow

Kenny Lau (May 02 2018 at 22:18):

theorem abs_pow {α : Type*} [decidable_linear_ordered_comm_ring α]
  (x : α) (n : nat) : abs (x^n) = (abs x)^n :=
nat.rec_on n abs_one $ λ n ih, (abs_mul _ _).trans $ congr_arg _ ih

Kenny Lau (May 02 2018 at 22:18):

but we all know what the answer is

Kenny Lau (May 02 2018 at 22:18):

this thing is in core

Mario Carneiro (May 02 2018 at 22:21):

Kenny, you need to work on making your issues more explicit. These code snippets don't speak for themselves

Kenny Lau (May 02 2018 at 22:23):

oh sorry

Kenny Lau (May 02 2018 at 22:23):

I mean, we should add this in our library

Chris Hughes (May 03 2018 at 08:10):

I think it's called pow_abs in mathlib

Kenny Lau (May 03 2018 at 08:10):

Kenny Lau (May 03 2018 at 08:11):

aha

Kenny Lau (May 03 2018 at 08:11):

very consistent naming

Last updated: Dec 20 2023 at 11:08 UTC