Commit 2020-10-19 11:39 0f1bc68f

View on Github →

feat(ring_theory/witt_vector/structure_polynomial): examples and basic properties (#4467) This is the 4th and final PR in a series on a fundamental theorem about Witt polynomials. Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Modified src/data/mv_polynomial/basic.lean

added theorem mv_polynomial.eval₂_hom_zero'

added theorem mv_polynomial.eval₂_hom_zero

Modified src/data/mv_polynomial/variables.lean

added theorem mv_polynomial.mem_vars_bind₁

added theorem mv_polynomial.mem_vars_rename

Modified src/ring_theory/witt_vector/structure_polynomial.lean

added theorem constant_coeff_witt_structure_int

added theorem constant_coeff_witt_structure_int_zero

added theorem constant_coeff_witt_structure_rat

added theorem constant_coeff_witt_structure_rat_zero

added theorem witt_vector.constant_coeff_witt_add

added theorem witt_vector.constant_coeff_witt_mul

added theorem witt_vector.constant_coeff_witt_neg

added theorem witt_vector.constant_coeff_witt_sub

added theorem witt_vector.witt_add_vars

added theorem witt_vector.witt_add_zero

added theorem witt_vector.witt_mul_vars

added theorem witt_vector.witt_mul_zero

added theorem witt_vector.witt_neg_vars

added theorem witt_vector.witt_neg_zero

added theorem witt_vector.witt_one_pos_eq_zero

added theorem witt_vector.witt_one_zero_eq_one

added theorem witt_vector.witt_structure_int_vars

added theorem witt_vector.witt_structure_rat_vars

added theorem witt_vector.witt_sub_zero

added theorem witt_vector.witt_zero_eq_zero