Commit 2022-08-16 10:36 791852eb

View on Github →

feat(polynomial/field_division): Add root_set_prod and clean up lemma statements (#16035) This PR adds root_set_prod (based on roots_prod) and cleans up lemma statements (the file already has {R S : Type*} [field R]).

Estimated changes

Modified src/data/polynomial/field_division.lean

modified theorem polynomial.mem_root_set

modified theorem polynomial.mem_roots_map

modified theorem polynomial.root_set_C_mul_X_pow

modified theorem polynomial.root_set_X_pow

modified theorem polynomial.root_set_monomial

added theorem polynomial.root_set_prod