lean语言证明|x * y| = |x| * |y|

在Lean语言中，我们可以使用以下代码来证明|x * y| = |x| * |y|：

import data.real.basic

theorem abs_mul_eq_mul_abs (x y : ℝ) : abs (x * y) = abs x * abs y :=
begin
  by_cases h1 : x ≥ 0,
  { by_cases h2 : y ≥ 0,
    { rw \[abs_of_nonneg h1, abs_of_nonneg h2, abs_of_nonneg (mul_nonneg h1 h2)\] },
    { rw \[abs_of_nonneg h1, abs_of_nonpos (mul_nonpos_of_nonneg_of_nonpos h1 h2)\] } },
  { by_cases h2 : y ≥ 0,
    { rw \[abs_of_nonpos (mul_nonpos_of_nonpos_of_nonneg h1 h2), abs_of_nonneg h2\] },
    { rw \[abs_of_nonpos (mul_nonneg_of_nonpos_of_nonpos h1 h2), abs_of_nonneg (mul_nonpos h1 h2)\] } }
end

这段代码使用了实数的基本性质和一些乘法的非负性质来进行证明。根据不同的情况，我们分别考虑了x和y的正负情况，并使用了abs_of_nonneg和abs_of_nonpos函数来表示绝对值的非负性质。最终，我们得到了|x * y| = |x| * |y|的证明。
#### 引用[.reference_title]
- *1* *2* *3* [定理证明自动化中的元编程问题](https://blog.csdn.net/pl_lab_001/article/details/118767769)[target="_blank" data-report-click={"spm":"1018.2226.3001.9630","extra":{"utm_source":"vip_chatgpt_common_search_pc_result","utm_medium":"distribute.pc_search_result.none-task-cask-2~all~insert_cask~default-1-null.142^v91^insert_down28v1,239^v3^insert_chatgpt"}} ] [.reference_item]
[ .reference_list ]