Division by zero in type theory: a FAQ 日本語訳これは 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 は / 記号を
