Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-30 00:12 af1290cb

View on Github →

feat(field_theory/ratfunc): rational functions as Laurent series (#11276)

Estimated changes

Modified src/field_theory/ratfunc.lean

added theorem ratfunc.algebra_map_apply

added theorem ratfunc.algebra_map_apply_div

added theorem ratfunc.coe_C

added theorem ratfunc.coe_X

added theorem ratfunc.coe_add

added def ratfunc.coe_alg_hom

added theorem ratfunc.coe_apply

added theorem ratfunc.coe_def

added theorem ratfunc.coe_div

added theorem ratfunc.coe_injective

added theorem ratfunc.coe_mul

added theorem ratfunc.coe_num_denom

added theorem ratfunc.coe_one

added theorem ratfunc.coe_smul

added theorem ratfunc.coe_zero

added theorem ratfunc.div_smul

added def ratfunc.lift_alg_hom

added theorem ratfunc.lift_alg_hom_apply

added theorem ratfunc.lift_alg_hom_apply_div

added theorem ratfunc.lift_alg_hom_apply_of_fraction_ring_mk

added theorem ratfunc.lift_alg_hom_injective

added def ratfunc.lift_monoid_with_zero_hom

added theorem ratfunc.lift_monoid_with_zero_hom_apply

added theorem ratfunc.lift_monoid_with_zero_hom_apply_div

added theorem ratfunc.lift_monoid_with_zero_hom_apply_of_fraction_ring_mk

added theorem ratfunc.lift_monoid_with_zero_hom_injective

added def ratfunc.lift_ring_hom

added theorem ratfunc.lift_ring_hom_apply

added theorem ratfunc.lift_ring_hom_apply_div

added theorem ratfunc.lift_ring_hom_apply_of_fraction_ring_mk

added theorem ratfunc.lift_ring_hom_injective

added theorem ratfunc.map_denom_ne_zero

added theorem ratfunc.smul_eq_C_mul

added theorem ratfunc.smul_eq_C_smul

Modified src/ring_theory/euclidean_domain.lean

added theorem gcd_ne_zero_of_left

added theorem gcd_ne_zero_of_right

Modified src/ring_theory/hahn_series.lean

added theorem hahn_series.algebra_map_apply'

added theorem polynomial.algebra_map_hahn_series_apply

added theorem polynomial.algebra_map_hahn_series_injective

Modified src/ring_theory/localization.lean

Modified src/ring_theory/power_series/basic.lean