Rev 2071 | Go to most recent revision | Details | Compare with Previous | Last modification | View Log | RSS feed
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 2071 | zjchen | 1 | eq:addnum addterm divnum exsides lincomb mulnum rewrite spliteq |
| 2 | eq/addnum:方程两边加上一个数 |
||
| 3 | eq/addterm:方程两边加一个代数式 |
||
| 4 | eq/divnum:方程除以非零数 |
||
| 5 | eq/exsides:交换方程的两边 |
||
| 6 | eq/lincomb:方程的加权和式 |
||
| 7 | eq/mulnum:用非零数乘方程 |
||
| 8 | eq/rewrite:重写方程 |
||
| 9 | eq/spliteq:根据(不)等式分解成各种情况 |
||
| 10 | exp:rewrite substit substitg |
||
| 11 | exp/rewrite:重写代数式 |
||
| 12 | exp/substit:整体或局部表达式内的替换 |
||
| 13 | exp/substitg:整体表达式内的替换 |
||
| 14 | ineq:addeqineq addineq addnum addterm constineq divexp divnum exsides lincomb mulexp mulineq mulnum obvineq rewrite simpdeduc splitineq sqrpos trans |
||
| 15 | ineq/addeqineq:不等式加一个等式 |
||
| 16 | ineq/addineq:两个不等式相加 |
||
| 17 | ineq/addnum:不等式两边加一个数 |
||
| 18 | ineq/addterm:不等式两边加代数式 |
||
| 19 | ineq/constineq:引入恒不等式 |
||
| 20 | ineq/divexp:用有恒定符号的代数式除不等式 |
||
| 21 | ineq/divnum:用非零数除不等式 |
||
| 22 | ineq/exsides:交换不等式的两边 |
||
| 23 | ineq/lincomb:不等式加权相加 |
||
| 24 | ineq/mulexp:用不变号代数式乘不等式 |
||
| 25 | ineq/mulineq:两个正值不等式相乘 |
||
| 26 | ineq/mulnum:用非零数乘不等式 |
||
| 27 | ineq/obvineq:用简单算术引进平凡不等式 |
||
| 28 | ineq/rewrite:重写不等式 |
||
| 29 | ineq/simpdeduc:不等式的简单推导 |
||
| 30 | ineq/splitineq:根据一不等式把情况分解 |
||
| 31 | ineq/sqrpos:实数的平方非负 |
||
| 32 | ineq/trans:应用不等式的传递性 |
||
| 33 | integrate:basic basic0 byparts chvar chvarinv const cut rewrite sincos |
||
| 34 | integrate/basic:基本积分公式 |
||
| 18479 | czzmrn | 35 | integrate/basic0:最少的基本积分公式 |
| 2071 | zjchen | 36 | integrate/byparts:分部积分 |
| 37 | integrate/chvar:变量的直接替换 |
||
| 38 | integrate/chvarinv:变量的逆替换 |
||
| 39 | integrate/const:常数的积分 |
||
| 40 | integrate/cut:把积分拆分为二 |
||
| 41 | integrate/rewrite:重写积分 |
||
| 42 | integrate/sincos:sin/cos/sh/ch的积分公式 |
||
| 43 | prf:cleanhyp contrapose splitgoal |
||
| 44 | prf/cleanhyp:删除无用的假设 |
||
| 45 | prf/contrapose:反证法 |
||
| 46 | prf/splitgoal:分离证明的目标 |