# Checking if expressions are equivalent, using certain equations

Let's say I have a bunch of formulas, and want to check if 2 expressions are the same, using those formulas:

Example:

```
F=m*a
W=F*s
m=rho*V
```

Now I would want to use something like full_simplify() on an expression like `W-rho*V*a*s`

, to check that `W`

and `rho*V*a*s`

are indeed equivalent.
I would like to be able to tell Sage which equations are allowed to be used for this simplification process

So polynomial equations/formulas?