Commit 2022-02-03 04:21 89a3c072

View on Github →

feat(field_theory/laurent): Laurent expansions of rational functions (#11199) Also provide more API for ratfunc, lifting homomorphisms of (polynomial to polynomial) to (ratfunc to ratfunc).

Estimated changes

Created src/field_theory/laurent.lean

added def ratfunc.laurent

added theorem ratfunc.laurent_C

added theorem ratfunc.laurent_X

added theorem ratfunc.laurent_algebra_map

added theorem ratfunc.laurent_at_zero

added def ratfunc.laurent_aux

added theorem ratfunc.laurent_aux_algebra_map

added theorem ratfunc.laurent_aux_div

added theorem ratfunc.laurent_aux_of_fraction_ring_mk

added theorem ratfunc.laurent_div

added theorem ratfunc.laurent_injective

added theorem ratfunc.laurent_laurent

added theorem ratfunc.taylor_mem_non_zero_divisors

Modified src/field_theory/ratfunc.lean

added theorem ratfunc.coe_map_alg_hom_eq_coe_map

added theorem ratfunc.coe_map_ring_hom_eq_coe_map

modified theorem ratfunc.div_smul

modified theorem ratfunc.lift_alg_hom_injective

modified def ratfunc.lift_monoid_with_zero_hom

modified theorem ratfunc.lift_monoid_with_zero_hom_apply_of_fraction_ring_mk

modified theorem ratfunc.lift_monoid_with_zero_hom_injective

modified def ratfunc.lift_ring_hom

modified theorem ratfunc.lift_ring_hom_apply_of_fraction_ring_mk

modified theorem ratfunc.lift_ring_hom_injective

added def ratfunc.map

added def ratfunc.map_alg_hom

added theorem ratfunc.map_apply

added theorem ratfunc.map_apply_div

added theorem ratfunc.map_apply_div_ne_zero

added theorem ratfunc.map_apply_of_fraction_ring_mk

added theorem ratfunc.map_injective

added def ratfunc.map_ring_hom

Modified src/ring_theory/hahn_series.lean

added theorem hahn_series.single_eq_zero_iff