Commit 2021-03-01 18:58 0faa7880

View on Github →

feat(ring_theory/hahn_series): introduce ring of Hahn series (#6237) Defines Hahn series Provides basic algebraic structure on Hahn series, up to comm_ring.

Estimated changes

Modified src/data/support.lean

added theorem function.support_smul_subset

added theorem pi.support_single

added theorem pi.support_single_of_ne

added theorem pi.support_single_subset

added theorem pi.support_single_zero

Created src/ring_theory/hahn_series.lean

added theorem hahn_series.add_coeff'

added theorem hahn_series.add_coeff

added theorem hahn_series.is_wf_support

added theorem hahn_series.mem_support

added theorem hahn_series.mul_coeff

added theorem hahn_series.mul_coeff_left'

added theorem hahn_series.mul_coeff_right'

added theorem hahn_series.mul_single_zero_coeff

added theorem hahn_series.neg_coeff'

added theorem hahn_series.neg_coeff

added theorem hahn_series.one_coeff

added def hahn_series.single

added theorem hahn_series.single_coeff

added theorem hahn_series.single_coeff_of_ne

added theorem hahn_series.single_coeff_same

added theorem hahn_series.single_eq_zero

added theorem hahn_series.single_zero_mul_eq_smul

added theorem hahn_series.single_zero_one

added theorem hahn_series.smul_coeff

added theorem hahn_series.sub_coeff'

added theorem hahn_series.sub_coeff

added def hahn_series.support

added theorem hahn_series.support_mul_subset_add_support

added theorem hahn_series.support_single_of_ne

added theorem hahn_series.support_zero

added theorem hahn_series.zero_coeff

added structure hahn_series