No, because x/y is just an arbitrary operation between x and y. Here you're assu... | Hacker News

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

		rnhmjoj 2 days ago \| parent \| context \| favorite \| on: Some Junk Theorems in Lean No, because x/y is just an arbitrary operation between x and y. Here you're assuming that 1/x is the inverse of x under *, but it's not.

orbifold 2 days ago [–]

I mean in a normal math curriculum you would define only the multiplicative inverse and then there is a separate way to define fraction, if you start out with certain rings. It is kind of surprising to me that they did a lazy definition of division.

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