Zulip Chat Archive
Stream: maths
Topic: inv_neg
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?
Kenny Lau (May 02 2020 at 09:32):
PR
Mario Carneiro (May 02 2020 at 09:33):
touche
Mario Carneiro (May 02 2020 at 09:34):
It's in mathlib, displaced from all the other theorems about division rings
Chris Hughes (May 02 2020 at 11:16):
Last updated: Dec 20 2023 at 11:08 UTC