Declarations generated by `simps`

Stream: mathlib4

[Riccardo Brasca]

The difference between docs#minpoly.Algebra.adjoin.powerBasis'_gen and docs3#algebra.adjoin.power_basis'_gen is rather impressive (I have an opened PR to fix the name difference, that is not a problem), and makes the first one unreadable and probably useless. We can of course add by hand the corresponding statement, but is there something better we can do here?

[Riccardo Brasca]

#5423