Commit 2019-07-22 11:20 fd916604
View on Github →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