Zulip Chat Archive

Stream: maths

Topic: inv_neg


view this post on Zulip Mario Carneiro (May 02 2020 at 09:31):

#check @inv_neg
-- inv_neg : ∀ {α : Type u_1} [_inst_1 : linear_ordered_field α] {a : α}, (-a)⁻¹ = -a⁻¹

Why is this a theorem about ordered fields?

view this post on Zulip Kenny Lau (May 02 2020 at 09:32):

PR

view this post on Zulip Mario Carneiro (May 02 2020 at 09:33):

touche

view this post on Zulip Mario Carneiro (May 02 2020 at 09:34):

It's in mathlib, displaced from all the other theorems about division rings

view this post on Zulip Chris Hughes (May 02 2020 at 11:16):

#2588


Last updated: May 06 2021 at 18:20 UTC