Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added theorem mv_power_series.C_add
added theorem mv_power_series.C_mul
added theorem mv_power_series.C_one
added theorem mv_power_series.C_zero
added theorem mv_power_series.ext
added theorem mv_power_series.map_id
added def mv_power_series
added def power_series.C
added theorem power_series.C_add
added theorem power_series.C_mul
added theorem power_series.C_one
added theorem power_series.C_zero
added def power_series.X
added theorem power_series.coeff_C
added theorem power_series.coeff_X'
added theorem power_series.coeff_X
added theorem power_series.coeff_add
added theorem power_series.coeff_inv
added theorem power_series.coeff_map
added theorem power_series.coeff_mk
added theorem power_series.coeff_mul
added theorem power_series.coeff_one
added theorem power_series.ext
added theorem power_series.ext_iff
added def power_series.map
added theorem power_series.map_add
added theorem power_series.map_comp
added theorem power_series.map_id
added theorem power_series.map_mul
added theorem power_series.map_one
added theorem power_series.map_zero
added def power_series.mk
added theorem power_series.trunc_C
added theorem power_series.trunc_add
added theorem power_series.trunc_one
added def power_series