mathlib3

ccf5188f - feat(ring_theory/power_basis): the dimension of a power basis is positive (#7638)

feat(ring_theory/power_basis): the dimension of a power basis is positive (#7638) We already have `pb.dim_ne_zero : pb.dim ≠ 0` (assuming nontriviality), but it's also useful to also have it in the form `0 < pb.dim`.