TheoremsaddUnits_neg_left, addUnits_neg_left_iff, addUnits_neg_right, addUnits_neg_right_iff, addUnits_of_val, addUnits_val, addUnits_val_iff, addUnits_zsmul_left, addUnits_zsmul_right, add_neg_eq_add_neg_iff_of_isAddUnit, isAddUnit_add_iff, neg_add_eq_neg_add_iff_of_isAddUnit, sub_eq_sub_iff_of_isAddUnit, addCommute_iff_add_neg_cancel, addCommute_iff_add_neg_cancel_assoc, addCommute_iff_neg_add_cancel, addCommute_iff_neg_add_cancel_assoc, nsmul_ofNSMulEqZero, val_neg_ofNSMulEqZero, val_ofNSMulEqZero, div_eq_div_iff_of_isUnit, inv_mul_eq_inv_mul_iff_of_isUnit, isUnit_mul_iff, mul_inv_eq_mul_inv_iff_of_isUnit, units_inv_left, units_inv_left_iff, units_inv_right, units_inv_right_iff, units_of_val, units_val, units_val_iff, units_zpow_left, units_zpow_right, of_nsmul_eq_zero, of_pow_eq_one, commute_iff_inv_mul_cancel, commute_iff_inv_mul_cancel_assoc, commute_iff_mul_inv_cancel, commute_iff_mul_inv_cancel_assoc, pow_ofPowEqOne, val_inv_ofPowEqOne, val_ofPowEqOne, isAddUnit_add_self_iff, isAddUnit_nsmul_iff, isAddUnit_nsmul_succ_iff, isUnit_mul_self_iff, isUnit_pow_iff, isUnit_pow_iff_of_not_isUnit, isUnit_pow_succ_iff | 49 |