Duplicate lemma

Stream: maths

[Thomas Browning]

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]

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

[Thomas Browning]

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]

The second name seems less guessable

[Bolton Bailey]

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

[Yaël Dillies]

_of_ne_zero, you mean? :stuck_out_tongue: