认领任务：在对应issue下评论然后在群里@subfish-zhou，我会invite you to be collaborator ！！注意！！请使用最新mathlib4 文件在MIL文件夹下，文本翻译格式遵循 https://github.com/avigad/mathematics_in_lean_source/?tab=readme-ov-file#markup 范例：https://github.com/Lean-zh/math-in-lean-zh/blob/master/MIL/C01_Introduction/S01_Getting_Started.lean 翻译规范（术语表，标点符号格式）：https://github.com/Agda-zh/PLFA-zh/issues/1 （本项目无法保留原文）
认领任务：在对应issue下评论然后在群里@subfish-zhou，我会invite you to be collaborator
！！注意！！请使用最新mathlib4
文件在MIL文件夹下，文本翻译格式遵循 https://github.com/avigad/mathematics_in_lean_source/?tab=readme-ov-file#markup
范例：https://github.com/Lean-zh/math-in-lean-zh/blob/master/MIL/C01_Introduction/S01_Getting_Started.lean
翻译规范（术语表，标点符号格式）：Agda-zh/PLFA-zh#1 （本项目无法保留原文）