Apologies, I meant for 0 \* inf = 0. Since in n \* inf n can be 0 the result sho... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		dependenttypes on July 7, 2020 \| parent \| context \| favorite \| on: Division by zero in type theory: a FAQ Apologies, I meant for 0 * inf = 0. Since in n * inf n can be 0 the result should be able to be 0.

somewhereoutth on July 7, 2020 [–]

You are correct - it should indeed be zero (and * can be constructed accordingly)

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact