!4#4169 LinearAlgebra.Matrix.Charpoly.Coeff

Stream: PR reviews

[Damiano Testa]

While preparing !4#4169 for porting, the unused variable linter pointed out that a have was unneeded. This was already the case in the original mathlib3 file.

Here are the two links to the relevant, unused, haves:

• in the original mathlib3,
• in the ported mathlib4.

Should I remove the have from both?

[Ruben Van de Velde]

I'd definitely remove it in mathlib 4, but it's probably not worth backporting

[Damiano Testa]

Ok, I left a porting note and I commented out the have: should I simply leave the porting note and remove the commented have?

[Eric Wieser]

Yeah, generally backporting proof lintfixes isn't worth it. Backporting statement fixes probably is, if that ever happens.

[Scott Morrison]

I wouldn't even leave a porting note for this, tbh.