Mathematica验证偏微分等式的输入输出正确性及文档查询问题

1. 输入代码是否对应命题 #

你的代码完全匹配命题的表述：

• 用z := f[a*x + b*y]定义了形式为一元函数f作用在线性组合ax+by上的二元函数z，符合命题的前提条件
• 用D[z, x]和D[z, y]分别计算z对x和y的偏导，代入运算的表达式和命题给出的b ∂z/∂x -a ∂z/∂y = 0完全一致。

2. 输出True是否表示命题成立 #

是的。Mathematica中==（Equal运算符）会自动对等式两侧做代数化简，当它返回True时，代表在通用默认假设（本题中即a、b为任意常数，f为任意可导一元函数）下，等式恒成立，和你纸笔推导的命题通用成立的结论一致。

3. 可参考的官方文档部分 #

以下几个核心内容的参考页可以解答你的疑问：

• D（偏导数计算函数）的参考页：明确偏导数的计算规则，验证你求偏导的操作逻辑正确
• Equal（==运算符）的参考页：说明==的求值逻辑，以及返回True、False、原等式三种结果的含义
• SetDelayed（:=运算符）的参考页：确认你定义z的延迟赋值方式不会提前求值，符合抽象函数定义的需求

4. 自行定位文档的方法 #

在Mathematica环境中可以通过两种方式快速定位：

• 选中你需要查询的函数、运算符（比如选中代码里的D或者==），按下F1键就会直接跳转到对应的官方参考页
• 打开帮助中心，在搜索框输入对应的关键词（比如“Equal 求值规则”“偏导数计算”）即可检索到对应文档

对照实验相关疑问解答 #

你的猜测是正确的。当==两侧的表达式既不能通过通用化简证明恒等，也不能证明互斥时，Mathematica会直接返回未求值的等式本身，这个返回结果的含义就是：你待验证的命题成立的充要条件为该等式成立。你修改参数后得到的等式只有当f的一阶导数恒为0时成立，也就是仅当f为常函数时命题成立，不符合通用成立的要求，刚好验证了你改参数后的命题不通用成立。
该规则的说明在Equal运算符参考页的「详细信息」板块。

内容的提问来源于stack exchange，提问作者Ron