mul_equiv.Pi_congr_right_refl

Stream: mathlib4

[Winston Yin]

Is there any reason why mul_equiv.Pi_congr_right_refl, mul_equiv.Pi_congr_right_symm, mul_equiv.Pi_congr_right_trans don't have to_additive attribute, while mul_equiv.Pi_congr_right does?

[Winston Yin]

The attribute can be added without error, so unless there's some special reason, I'm going to add to_additive back in during porting algebra.hom.equiv.basic

[Ruben Van de Velde]

Did it exist in 3 and not get ported?

[Winston Yin]

It didn’t exist in 3. See docs#mul_equiv.Pi_congr_right_refl but there’s no add_equiv. Pi_congr_right_refl

[Eric Wieser]

Why not make a PR to mathlib 3 to add it?

[Kevin Buzzard]

That way you'll find out if it causes any problems