Rev 16103 | Go to most recent revision | Details | Last modification | View Log | RSS feed
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 20 | reyssat | 1 | eq/addnum:Ajouter un nombre aux deux côtés d'une équation |
| 2 | eq/addterm:Ajouter une expression aux deux côtés d'une équation |
||
| 3 | eq/divnum:Diviser une équation par un nombre non-nul |
||
| 4 | eq/exsides:Echanger les deux côtés d'une équation |
||
| 5 | eq/lincomb:Addition d'équations avec coefficients |
||
| 6 | eq/mulnum:Multiplier une équation par un nombre non-nul |
||
| 7 | eq/rewrite:Réécrire une équation |
||
| 8 | eq/spliteq:Séparer les cas selon une (in)équation |
||
| 9 | eq: addnum addterm divnum exsides lincomb mulnum rewrite spliteq |
||
| 10 | exp/rewrite:Réécriture algébrique d'une expression |
||
| 11 | exp/substit:Substitution dans une expression algébrique globale ou partielle |
||
| 12 | exp/substitg:Substitution dans une expression globale |
||
| 13 | exp: rewrite substit substitg |
||
| 14 | ineq/addeqineq:Ajouter une équation à une inégalité |
||
| 15 | ineq/addineq:Ajouter deux inégalités |
||
| 16 | ineq/addnum:Ajouter un nombre aux deux côtés d'une inégalité |
||
| 17 | ineq/addterm:Ajouter une expression aux deux côtés d'une inégalité |
||
| 18 | ineq/constineq:Introduire une inégalité constante |
||
| 19 | ineq/divexp:Diviser une inégalité par une expression à signe constant |
||
| 20 | ineq/divnum:Diviser une inégalité par un nombre non-nul |
||
| 21 | ineq/exsides:Echanger les deux côtés d'une inégalité |
||
| 22 | ineq/lincomb:Addition d'inégalités avec coefficients |
||
| 23 | ineq/mulexp:Multiplier une inégalité par une expression à signe constant |
||
| 24 | ineq/mulineq:Multiplier deux inégalités positives |
||
| 25 | ineq/mulnum:Multiplier une inégalité par un nombre non-nul |
||
| 26 | ineq/obvineq:Introduire une inégalité évidente par simple arithmétique |
||
| 27 | ineq/rewrite:Réécrire une inégalité |
||
| 28 | ineq/simpdeduc:Simple déduction d'inégalité |
||
| 29 | ineq/splitineq:Séparer les cas selon une inégalité |
||
| 30 | ineq/sqrpos:Le carré d'un nombre réel est positif ou nul |
||
| 31 | ineq/trans:Appliquer la transitivité des inégalités |
||
| 32 | ineq: addeqineq addineq addnum addterm constineq divexp divnum exsides lincomb mulexp mulineq mulnum obvineq rewrite simpdeduc splitineq sqrpos trans |
||
| 33 | integrate/basic:Formule d'intégration de base |
||
| 34 | integrate/basic0:Formule d'intégration de base minimale |
||
| 35 | integrate/byparts:Intégration par parties |
||
| 36 | integrate/chvar:Changement de variable direct |
||
| 37 | integrate/chvarinv:Changement de variable inverse |
||
| 38 | integrate/const:Intégration d'une constante |
||
| 39 | integrate/cut:Couper une intégration en deux |
||
| 40 | integrate/rewrite:Réécrire une intégrale |
||
| 41 | integrate/sincos:Formule d'intégration de sin/cos/sh/ch |
||
| 42 | integrate: basic basic0 byparts chvar chvarinv const cut rewrite sincos |
||
| 43 | prf/cleanhyp:Effacer des hypothèses inutiles |
||
| 44 | prf/contrapose:Contraposer |
||
| 45 | prf/splitgoal:Montrer un but séparément (quand il y en a plusieurs) |
||
| 46 | prf: cleanhyp contrapose splitgoal |