Details | Last modification | View Log | RSS feed
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 20 | reyssat | 1 | eq/addnum:Add a number to the two sides of an equation |
| 2 | eq/addterm:Add an expression to the two sides of an equation |
||
| 3 | eq/divnum:Divisde an equation by a number |
||
| 4 | eq/exsides:Exchange the two sides of an equation |
||
| 5 | eq/lincomb:Addition of equations with coefficients |
||
| 6 | eq/mulnum:Multiply an equation by a number |
||
| 7 | eq/rewrite:Rewrite an equation |
||
| 8 | eq/spliteq:Separate the cases according to an (in)equation |
||
| 9 | exp/rewrite:Rewrite an expression |
||
| 10 | exp/substit:Substitution in an expression |
||
| 11 | exp/substitg:Substitution in an expression |
||
| 12 | ineq/addeqineq:Add an equation to an inequality |
||
| 13 | ineq/addineq:Add two inequalities |
||
| 14 | ineq/addnum:Add a number to the two sides of an inequality |
||
| 15 | ineq/addterm:Add an expression to the two sides of an inequality |
||
| 16 | ineq/constineq:Introduce a constant inequality |
||
| 17 | ineq/divexp:Divide an inequality by an expression |
||
| 18 | ineq/divnum:Divide an inequality by a number |
||
| 19 | ineq/exsides:Exchange the two sides of an inequality |
||
| 20 | ineq/lincomb:Addition of inequalities with coefficients |
||
| 21 | ineq/mulexp:Multiply an inequality by an expression |
||
| 22 | ineq/mulineq:Multiply two inequalities |
||
| 23 | ineq/mulnum:Multiply an inequality by a number |
||
| 24 | ineq/obvineq:Introduce an obvious inequality |
||
| 25 | ineq/rewrite:Rewrite an inequality |
||
| 26 | ineq/simpdeduc:Simple deduction of inequality |
||
| 27 | ineq/splitineq:Separate cases according to an inequality |
||
| 28 | ineq/sqrpos:Positivity of a square |
||
| 29 | ineq/trans:Transitivity of inequalities |
||
| 30 | integrate/basic:Basic integration formula |
||
| 31 | integrate/basic0:Basic integration formula |
||
| 32 | integrate/byparts:Integration by parts |
||
| 33 | integrate/chvar:Direct change of variable |
||
| 34 | integrate/chvarinv:Reverse change of variable |
||
| 35 | integrate/const:Integration of a constant |
||
| 36 | integrate/cut:Cut an integration into two |
||
| 37 | integrate/rewrite:Rewrite an integral |
||
| 38 | integrate/sincos:Integration formula of sin/cos/sh/ch |
||
| 39 | prf/cleanhyp:Erase useless hypotheses |
||
| 40 | prf/contrapose:Contrapose |
||
| 41 | prf/splitgoal:Prove a goal separately (when there are several) |