mathlib3

fd916604 - feat(data/power_series): Add multivariate power series and prove basic API (#1244)

feat(data/power_series): Add multivariate power series and prove basic API (#1244) * First start on power_series * Innocent changes * Almost a comm_semiring * Defined hom from mv_polynomial to mv_power_series; sorrys remain * Attempt that seem to go nowhere * Working on coeff_mul for polynomials * Small progress * Finish mv_polynomial.coeff_mul * Cleaner proof of mv_polynomial.coeff_mul * Fix build * WIP * Finish proof of mul_assoc * WIP * Golfing coeff_mul * WIP * Crazy wf is crazy * mv_power_series over local ring is local * WIP * Add empty line * wip * wip * WIP * WIP * WIP * Add header comments * WIP * WIP * Fix finsupp build * Fix build, hopefully * Fix build: ideals * More docs * Update src/data/power_series.lean Fix typo. * Fix build -- bump instance search depth * Make changes according to some of the review comments * Use 'formal' in the names * Use 'protected' in more places, remove '@simp's * Make 'inv_eq_zero' an iff * Generalize to non-commutative scalars * Move file * Undo name change, back to 'power_series' * spelling mistake * spelling mistake