Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 20:38 8d2e8871

View on Github →

feat(number_theory/function_field): add place at infinity (#12245)

Estimated changes

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.nat_degree_sub_eq_of_prod_eq

Modified src/field_theory/ratfunc.lean

added theorem ratfunc.X_ne_zero

added def ratfunc.int_degree

added theorem ratfunc.int_degree_C

added theorem ratfunc.int_degree_X

added theorem ratfunc.int_degree_add

added theorem ratfunc.int_degree_add_le

added theorem ratfunc.int_degree_mul

added theorem ratfunc.int_degree_neg

added theorem ratfunc.int_degree_one

added theorem ratfunc.int_degree_polynomial

added theorem ratfunc.int_degree_zero

added theorem ratfunc.nat_degree_num_mul_right_sub_nat_degree_denom_mul_left_eq_int_degree

added theorem ratfunc.num_denom_neg

added theorem ratfunc.num_mul_denom_add_denom_mul_num_ne_zero

Modified src/number_theory/function_field.lean

added theorem function_field.infty_valuation.C

added theorem function_field.infty_valuation.X

added theorem function_field.infty_valuation.map_add_le_max'

added theorem function_field.infty_valuation.map_mul'

added theorem function_field.infty_valuation.map_one'

added theorem function_field.infty_valuation.map_zero'

added theorem function_field.infty_valuation.polynomial

added def function_field.infty_valuation

added theorem function_field.infty_valuation_apply

added def function_field.infty_valuation_def

added theorem function_field.infty_valuation_of_nonzero