Commit 2023-05-25 21:39 83f97af5

View on Github →

feat: port FieldTheory.Ratfunc (#4293) I am going to try to work on this for a bit, but it looks hard.

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.coe_C
added theorem RatFunc.coe_X
added theorem RatFunc.coe_add
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_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 def RatFunc.denom
added theorem RatFunc.denom_C
added theorem RatFunc.denom_X
added theorem RatFunc.denom_add_dvd
added theorem RatFunc.denom_div
added theorem RatFunc.denom_div_dvd
added theorem RatFunc.denom_dvd
added theorem RatFunc.denom_mul_dvd
added theorem RatFunc.denom_ne_zero
added theorem RatFunc.denom_one
added theorem RatFunc.denom_zero
added theorem RatFunc.div_smul
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.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.liftOn'_div
added theorem RatFunc.liftOn'_mk
added theorem RatFunc.liftOn_div
added theorem RatFunc.liftOn_mk
added def RatFunc.map
added theorem RatFunc.map_apply
added theorem RatFunc.map_apply_div
added theorem RatFunc.map_injective
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_div
added theorem RatFunc.mk_eq_mk
added theorem RatFunc.mk_one'
added theorem RatFunc.mk_one
added theorem RatFunc.mk_smul
added theorem RatFunc.mk_zero
added theorem RatFunc.monic_denom
added theorem RatFunc.mul_inv_cancel
added def RatFunc.num
added def RatFunc.numDenom
added theorem RatFunc.numDenom_div
added theorem RatFunc.num_C
added theorem RatFunc.num_X
added theorem RatFunc.num_algebraMap
added theorem RatFunc.num_denom_add
added theorem RatFunc.num_denom_mul
added theorem RatFunc.num_denom_neg
added theorem RatFunc.num_div
added theorem RatFunc.num_div_denom
added theorem RatFunc.num_div_dvd'
added theorem RatFunc.num_div_dvd
added theorem RatFunc.num_dvd
added theorem RatFunc.num_mul_dvd
added theorem RatFunc.num_ne_zero
added theorem RatFunc.num_one
added theorem RatFunc.num_zero
added theorem RatFunc.smul_eq_C_mul
added theorem RatFunc.smul_eq_C_smul
added structure RatFunc