Zulip Chat Archive

Stream: general

Topic: order of input variables

Kevin Buzzard (Jan 31 2020 at 02:36):

lemma eq_inv_mul_of_mul_eq {α : Type*} [group α] {a b c : α} : b * a = c  a = b⁻¹ * c

This is in core. More natural notation for mathematicians might be

{a x y : G} : a * x = y → x = a⁻¹ * y

but this is not quite alpha equivalent because the equivalent term has variables ordered x a y which sort of looks bonkers. Does this sort of thing matter? Does it break all the AI's if I switch them?

Last updated: Aug 03 2023 at 10:10 UTC