Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-30 08:55 c6fab42c

View on Github →

feat(ring_theory/power_series): order (#1292)

  • 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
  • Order of a power series
  • Start on formal Laurent series
  • WIP
  • Remove file. It's for another PR.
  • Add stuff about order
  • Remove old file
  • Basics on order of power series
  • Lots of stuff
  • Move stuff on kernels
  • Move stuff on ker to the right place
  • Fix build
  • Add elim_cast attributes, update documentation
  • Bundle homs
  • Fix build
  • Remove duplicate trunc_C
  • Fix build

Estimated changes

added theorem is_ring_hom.mem_ker
added theorem mv_polynomial.coe_C
added theorem mv_polynomial.coe_X
added theorem mv_polynomial.coe_add
added theorem mv_polynomial.coe_mul
added theorem mv_polynomial.coe_one
added theorem mv_polynomial.coe_zero
modified def mv_power_series.C
deleted theorem mv_power_series.C_add
deleted theorem mv_power_series.C_mul
deleted theorem mv_power_series.C_one
deleted theorem mv_power_series.C_zero
modified def mv_power_series.X
added theorem mv_power_series.X_def
added theorem mv_power_series.X_inj
modified def mv_power_series.coeff
deleted theorem mv_power_series.coeff_X''
deleted theorem mv_power_series.coeff_X'
deleted theorem mv_power_series.coeff_add
modified theorem mv_power_series.coeff_inv
modified theorem mv_power_series.coeff_map
modified theorem mv_power_series.coeff_mul
deleted theorem mv_power_series.coeff_neg
modified theorem mv_power_series.coeff_one
modified theorem mv_power_series.coeff_trunc
modified theorem mv_power_series.coeff_zero
modified theorem mv_power_series.ext
modified def mv_power_series.map
deleted theorem mv_power_series.map_add
modified theorem mv_power_series.map_comp
modified theorem mv_power_series.map_id
deleted theorem mv_power_series.map_mul
deleted theorem mv_power_series.map_one
deleted theorem mv_power_series.map_zero
modified def mv_power_series.trunc
modified theorem mv_power_series.trunc_C
deleted theorem mv_power_series.trunc_add
modified theorem mv_power_series.trunc_one
added theorem polynomial.coe_C
added theorem polynomial.coe_X
added theorem polynomial.coe_add
added theorem polynomial.coe_mul
added theorem polynomial.coe_one
added theorem polynomial.coe_zero
added theorem polynomial.coeff_coe
modified def power_series.C
deleted theorem power_series.C_add
deleted theorem power_series.C_mul
deleted theorem power_series.C_one
deleted theorem power_series.C_zero
added theorem power_series.X_dvd_iff
added theorem power_series.X_eq
added theorem power_series.X_pow_eq
added theorem power_series.X_prime
modified def power_series.coeff
deleted theorem power_series.coeff_C_zero
deleted theorem power_series.coeff_X'
deleted theorem power_series.coeff_add
added theorem power_series.coeff_def
modified theorem power_series.coeff_mk
deleted theorem power_series.coeff_zero
modified theorem power_series.ext
modified theorem power_series.ext_iff
modified theorem power_series.inv_of_unit_eq
modified def power_series.map
deleted theorem power_series.map_add
modified theorem power_series.map_comp
modified theorem power_series.map_id
deleted theorem power_series.map_mul
deleted theorem power_series.map_one
deleted theorem power_series.map_zero
modified def power_series.monomial
deleted theorem power_series.monomial_add
added theorem power_series.order_X
added theorem power_series.order_eq
added theorem power_series.order_ge
added theorem power_series.order_le
added theorem power_series.order_mul
added theorem power_series.order_one
modified theorem power_series.trunc_C