Commit 2024-03-12 11:06 a979c461

View on Github →

feat(NumberTheory/LSeries/Linearity): move/add statements on linearity of L-series (#11214) This adds a file NumberTheory.LSeries.Linearity, which contains statements on

  • addition (moved from NumberTheory.LSeries.Basic)
  • negation and
  • scalar multiplication of L-series, and corresponding statements for LSeries.term, LSeriesHasSum and LSeriesSummable. See this thread on Zulip.

Estimated changes

deleted theorem LSeries.term_add
deleted theorem LSeries.term_add_apply
deleted theorem LSeriesHasSum_add
deleted theorem LSeriesSummable_add
deleted theorem LSeries_add
added theorem LSeries.term_add
added theorem LSeries.term_add_apply
added theorem LSeries.term_neg
added theorem LSeries.term_neg_apply
added theorem LSeries.term_smul
added theorem LSeries.term_sub
added theorem LSeries.term_sub_apply
added theorem LSeriesHasSum.add
added theorem LSeriesHasSum.neg
added theorem LSeriesHasSum.smul
added theorem LSeriesHasSum.sub
added theorem LSeriesSummable.add
added theorem LSeriesSummable.neg
added theorem LSeriesSummable.smul
added theorem LSeriesSummable.sub
added theorem LSeries_add
added theorem LSeries_neg
added theorem LSeries_smul
added theorem LSeries_sub