Commit 2021-03-10 11:57 e221dc9a

View on Github →

feat(ring_theory/hahn_series): algebra structure, equivalences with power series (#6540) Places an algebra structure on hahn_series Defines a ring_equiv and when relevant an alg_equiv between hahn_series nat R and power_series R.

Estimated changes

Modified src/data/polynomial/algebra_map.lean

Modified src/order/well_founded_set.lean

added theorem set.is_wf_univ_iff

added theorem well_founded.is_wf

Modified src/ring_theory/hahn_series.lean

added def hahn_series.C

added theorem hahn_series.C_apply

added theorem hahn_series.C_eq_algebra_map

added theorem hahn_series.C_mul_eq_smul

added theorem hahn_series.C_one

added theorem hahn_series.C_zero

modified theorem hahn_series.add_coeff'

modified theorem hahn_series.add_coeff

added theorem hahn_series.algebra_map_apply

added theorem hahn_series.coeff_to_power_series

added theorem hahn_series.coeff_to_power_series_symm

added theorem hahn_series.eq_of_mem_support_single

added theorem hahn_series.mul_single_coeff_add

added def hahn_series.single.add_monoid_hom

added theorem hahn_series.single.add_monoid_hom_apply

added def hahn_series.single.linear_map

added theorem hahn_series.single.linear_map_apply

modified def hahn_series.single

modified theorem hahn_series.single_eq_zero

added theorem hahn_series.single_mul_coeff_add

added theorem hahn_series.single_mul_single

added theorem hahn_series.single_zero_mul_coeff

added theorem hahn_series.support_single_subset

added def hahn_series.to_power_series

added def hahn_series.to_power_series_alg

added theorem hahn_series.to_power_series_alg_apply

added theorem hahn_series.to_power_series_alg_symm_apply

Modified src/ring_theory/power_series/basic.lean

added theorem mv_power_series.C_eq_algebra_map

added theorem mv_power_series.algebra_map_apply

added theorem power_series.C_eq_algebra_map

added theorem power_series.algebra_map_apply