Commit 2025-01-31 18:21 3ebdb300

View on Github →

chore (RingTheory/HahnSeries): fix names that use coeff (#21279) Basic pattern: (n • x).coeff = n • x.coeff was named nsmul_coeff but it should be coeff_nsmul.

Estimated changes

deleted theorem HVertexOperator.add_coeff
deleted theorem HahnSeries.add_coeff'
deleted theorem HahnSeries.add_coeff
added theorem HahnSeries.coeff_add'
added theorem HahnSeries.coeff_add
added theorem HahnSeries.coeff_neg'
added theorem HahnSeries.coeff_neg
added theorem HahnSeries.coeff_nsmul
added theorem HahnSeries.coeff_smul
added theorem HahnSeries.coeff_sub'
added theorem HahnSeries.coeff_sub
deleted theorem HahnSeries.neg_coeff'
deleted theorem HahnSeries.neg_coeff
deleted theorem HahnSeries.nsmul_coeff
deleted theorem HahnSeries.smul_coeff
deleted theorem HahnSeries.sub_coeff'
deleted theorem HahnSeries.sub_coeff
added theorem HahnSeries.coeff_zero
deleted theorem HahnSeries.single_coeff
deleted theorem HahnSeries.zero_coeff
added theorem HahnModule.coeff_smul
deleted theorem HahnModule.smul_coeff
added theorem HahnSeries.coeff_mul
added theorem HahnSeries.coeff_one
deleted theorem HahnSeries.mul_coeff
deleted theorem HahnSeries.one_coeff