Commit 2024-05-20 10:05 b2214f73

View on Github →

chore(FieldTheory/RatFunc): split the file into several ones (#12425) Following the discussion in #12245 I am splitting FieldTheory/RatFunc into several files. A new folder RatFunc is created in the parent FieldTheory together with the files

  • Basic containing all basic definitions (lines 1-295)
  • FieldStructure containing results about the field structure with numerators and denominators (lines 296-1381)
  • FunLike containing properties about rational functions as functions (lines 1382-1558)
  • Degree with properties about the degree (lines 1560-1657) Lines 1658 to the end are moved to RingTheory/LaurentSeries .

Estimated changes

added def RatFunc.C
added def RatFunc.X
added theorem RatFunc.X_ne_zero
added theorem RatFunc.algebraMap_C
added theorem RatFunc.algebraMap_X
added theorem RatFunc.denom_C
added theorem RatFunc.denom_X
added def RatFunc.eval
added theorem RatFunc.eval_C
added theorem RatFunc.eval_X
added theorem RatFunc.eval_add
added theorem RatFunc.eval_mul
added theorem RatFunc.eval_one
added theorem RatFunc.eval_zero
added theorem RatFunc.num_C
added theorem RatFunc.num_X
added theorem RatFunc.smul_eq_C_mul
deleted def RatFunc.C
deleted def RatFunc.X
deleted theorem RatFunc.X_ne_zero
deleted theorem RatFunc.algebraMap_C
deleted theorem RatFunc.algebraMap_X
deleted theorem RatFunc.algebraMap_comp_C
deleted theorem RatFunc.algebraMap_eq_C
deleted def RatFunc.coeAlgHom
deleted theorem RatFunc.coe_C
deleted theorem RatFunc.coe_X
deleted theorem RatFunc.coe_add
deleted theorem RatFunc.coe_apply
deleted theorem RatFunc.coe_coe
deleted theorem RatFunc.coe_def
deleted theorem RatFunc.coe_div
deleted theorem RatFunc.coe_injective
deleted theorem RatFunc.coe_mul
deleted theorem RatFunc.coe_ne_zero
deleted theorem RatFunc.coe_neg
deleted theorem RatFunc.coe_num_denom
deleted theorem RatFunc.coe_one
deleted theorem RatFunc.coe_pow
deleted theorem RatFunc.coe_smul
deleted theorem RatFunc.coe_sub
deleted theorem RatFunc.coe_zero
deleted theorem RatFunc.denom_C
deleted theorem RatFunc.denom_X
deleted def RatFunc.eval
deleted theorem RatFunc.eval_C
deleted theorem RatFunc.eval_X
deleted theorem RatFunc.eval_add
deleted theorem RatFunc.eval_algebraMap
deleted theorem RatFunc.eval_mul
deleted theorem RatFunc.eval_one
deleted theorem RatFunc.eval_zero
deleted def RatFunc.intDegree
deleted theorem RatFunc.intDegree_C
deleted theorem RatFunc.intDegree_X
deleted theorem RatFunc.intDegree_add
deleted theorem RatFunc.intDegree_add_le
deleted theorem RatFunc.intDegree_mul
deleted theorem RatFunc.intDegree_neg
deleted theorem RatFunc.intDegree_one
deleted theorem RatFunc.intDegree_zero
deleted theorem RatFunc.liftOn'_mk
deleted theorem RatFunc.liftOn_mk
deleted theorem RatFunc.mk_coe_def
deleted theorem RatFunc.mk_def_of_mem
deleted theorem RatFunc.mk_def_of_ne
deleted theorem RatFunc.mk_eq_div'
deleted theorem RatFunc.mk_eq_mk
deleted theorem RatFunc.mk_one'
deleted theorem RatFunc.mk_zero
deleted theorem RatFunc.num_C
deleted theorem RatFunc.num_X
deleted theorem RatFunc.single_inv
deleted theorem RatFunc.single_one_eq_pow
deleted theorem RatFunc.single_zpow
deleted theorem RatFunc.smul_eq_C_mul
deleted structure RatFunc
added theorem RatFunc.liftOn'_mk
added theorem RatFunc.liftOn_mk
added theorem RatFunc.mk_coe_def
added theorem RatFunc.mk_def_of_mem
added theorem RatFunc.mk_def_of_ne
added theorem RatFunc.mk_eq_div'
added theorem RatFunc.mk_eq_mk
added theorem RatFunc.mk_one'
added theorem RatFunc.mk_zero
added structure RatFunc
added theorem RatFunc.intDegree_C
added theorem RatFunc.intDegree_X
added theorem RatFunc.intDegree_add
added theorem RatFunc.intDegree_mul
added theorem RatFunc.intDegree_neg
added theorem RatFunc.intDegree_one
added theorem RatFunc.intDegree_zero
added theorem RatFunc.coe_C
added theorem RatFunc.coe_X
added theorem RatFunc.coe_add
added theorem RatFunc.coe_apply
added theorem RatFunc.coe_coe
added theorem RatFunc.coe_def
added theorem RatFunc.coe_div
added theorem RatFunc.coe_injective
added theorem RatFunc.coe_mul
added theorem RatFunc.coe_ne_zero
added theorem RatFunc.coe_neg
added theorem RatFunc.coe_num_denom
added theorem RatFunc.coe_one
added theorem RatFunc.coe_pow
added theorem RatFunc.coe_smul
added theorem RatFunc.coe_sub
added theorem RatFunc.coe_zero
added theorem RatFunc.single_inv
added theorem RatFunc.single_zpow