Commit 2023-01-15 13:24 3afdc9ee

fix: prove sorries in Tactic.NormNum.Basic (#1572)

• I slightly simplified the statement of isRat_inv_pos and isRat_inv_neg to not need a positivity assumption.
• The statements of isRat_add, isRat_sub, isRat_mul did not need to assume the multiplier k is nonzero.
• The statement of isRat_inv_pos was also wrong, needing a CharZero assumption. We can revisit the possibility of non-CharZero rings later (by taking an Invertible n assumption there instead).