Zulip Chat Archive

Stream: maths

Topic: Duplicate lemma


Thomas Browning (Feb 10 2022 at 07:31):

Is there any particular reason why mathlib has this duplicate lemma in algebra/groups/defs?

@[simp, to_additive]
lemma mul_right_inv (a : G) : a * a⁻¹ = 1 :=
have a⁻¹⁻¹ * a⁻¹ = 1 := mul_left_inv a⁻¹,
by rwa [inv_inv] at this

@[to_additive] lemma mul_inv_self (a : G) : a * a⁻¹ = 1 := mul_right_inv a

Mario Carneiro (Feb 10 2022 at 07:39):

because sometimes people have multiple guesses for what the name could be

Thomas Browning (May 12 2022 at 03:35):

Here's a pair of duplicate lemmas:
docs#polynomial.support_C_mul_X_pow_nonzero
docs#polynomial.support_mul_X_pow
Should one of these be deleted? Which one?

Alex J. Best (May 12 2022 at 07:44):

The second name seems less guessable

Bolton Bailey (May 13 2022 at 06:37):

The first one should probably be "...of_nonzero"

Yaël Dillies (May 13 2022 at 07:50):

_of_ne_zero, you mean? :stuck_out_tongue:


Last updated: Dec 20 2023 at 11:08 UTC