これは Xena の記事の有志による非公式翻訳です. 原文は Division by zero in type theory: a FAQ です. 翻訳に際して,機械翻訳サービスDeepL翻訳を参考にしました. ねえ, Lean では 1/0=0 だって聞いたんだけど, 本当? 本当ですよ.Coq や Agda,その他多くの証明支援系と同じです. それは矛盾にならないの? いいえ.Lean の / 記号が数学的な割り算を意味しないというだけです.\mathbb{R} を実数全体とします.関数 f:\mathbb{R}^2\to\mathbb{R} を y\not=0 に対しては f(x,y)=x/y であり,y=0 のとき f(x,0)=0 を満たすようなものとして定義します.この定義が数学に矛盾をもたらすでしょうか?もちろんそんなことはありません!単なる定義です.Lean は / 記号を
![Division by zero in type theory: a FAQ 日本語訳](https://cdn-ak-scissors.b.st-hatena.com/image/square/21039cc20bdb0ba4a5b752d3eaecd5cb46952007/height=288;version=1;width=512/https%3A%2F%2Fres.cloudinary.com%2Fzenn%2Fimage%2Fupload%2Fs--oBExcrBl--%2Fc_fit%252Cg_north_west%252Cl_text%3Anotosansjp-medium.otf_55%3ADivision%252520by%252520zero%252520in%252520type%252520theory%25253A%252520a%252520FAQ%252520%2525E6%252597%2525A5%2525E6%25259C%2525AC%2525E8%2525AA%25259E%2525E8%2525A8%2525B3%252Cw_1010%252Cx_90%252Cy_100%2Fg_south_west%252Cl_text%3Anotosansjp-medium.otf_37%3Alean%252520ja%252Cx_203%252Cy_121%2Fg_south_west%252Ch_90%252Cl_fetch%3AaHR0cHM6Ly9saDMuZ29vZ2xldXNlcmNvbnRlbnQuY29tL2EvQUNnOG9jSmd4c1lrQlhDNm9pVzliN2oyaU1DZHFRN3lGNjJGQTNKT3ltWnNoMFBhOXc9czk2LWM%3D%252Cr_max%252Cw_90%252Cx_87%252Cy_95%2Fv1627283836%2Fdefault%2Fog-base-w1200-v2.png)