mathlib3

d1d69e99 - feat(ring_theory/power_basis): matrix of multiplication by generator (#18177)

feat(ring_theory/power_basis): matrix of multiplication by generator (#18177) + `power_basis.left_mul_matrix` computes the matrix of left multiplication by the generator with respect to the power basis: the last column is the negation of the coefficients of the minimal polynomial, while in other columns there are 1's below the diagonal and 0 elsewhere. + Also generalizes `comm_ring` or `field` in other files to `ring` where possible.