Commit 2021-05-14 12:59 adb0f6e0

View on Github →

feat(Algebra/*): beginning of algebra hierarchy (#4)

Estimated changes

added theorem add_add_add_comm
added theorem add_left_comm
added theorem add_right_comm
added theorem add_right_eq_self
added theorem mul_left_comm
added theorem mul_mul_mul_comm
added theorem mul_right_comm
added theorem self_eq_add_right
added theorem add_assoc
added theorem add_comm
added theorem add_left_cancel
added theorem add_left_cancel_iff
added theorem add_left_inj
added theorem add_left_neg
added theorem add_neg_cancel_right
added theorem add_neg_self
added theorem add_right_cancel
added theorem add_right_cancel_iff
added theorem add_right_inj
added theorem add_right_neg
added theorem add_zero
added def gpow_rec
added def gsmul_rec
added theorem inv_eq_of_mul_eq_one
added theorem inv_inv
added theorem inv_mul_cancel_left
added theorem inv_mul_self
added theorem left_inv_eq_right_inv
added theorem left_neg_eq_right_neg
added theorem mul_assoc
added theorem mul_comm
added theorem mul_inv_cancel_right
added theorem mul_inv_self
added theorem mul_left_cancel
added theorem mul_left_cancel_iff
added theorem mul_left_inj
added theorem mul_left_inv
added theorem mul_one
added theorem mul_right_cancel
added theorem mul_right_cancel_iff
added theorem mul_right_inj
added theorem mul_right_inv
added theorem neg_add_cancel_left
added theorem neg_add_self
added theorem neg_eq_of_add_eq_zero
added theorem neg_neg
added def npow_rec
added def nsmul_rec
added theorem one_mul
added theorem zero_add