Commit 2022-12-14 09:49 d1e1c996

View on Github →

feat port Algebra.Field.Basic (#975) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

added theorem add_div'
added theorem add_div
added theorem add_div_eq_mul_add_div
added theorem div_add'
added theorem div_add_div
added theorem div_add_div_same
added theorem div_add_one
added theorem div_add_same
added theorem div_neg
added theorem div_neg_eq_neg_div
added theorem div_neg_self
added theorem div_sub'
added theorem div_sub_div
added theorem div_sub_div_same
added theorem div_sub_one
added theorem div_sub_same
added theorem inv_add_inv
added theorem inv_neg
added theorem inv_sub_inv'
added theorem inv_sub_inv
added theorem neg_div'
added theorem neg_div
added theorem neg_div_neg_eq
added theorem neg_div_self
added theorem neg_inv
added theorem of_dual_rat_cast
added theorem of_lex_rat_cast
added theorem one_add_div
added theorem one_div_add_one_div
added theorem one_sub_div
added theorem same_add_div
added theorem same_sub_div
added theorem sub_div'
added theorem sub_div
added theorem to_dual_rat_cast
added theorem to_lex_rat_cast