search

metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

ax-mulcom pr 9 (mulgt0 results) #4061

Closed icecream17 closed 3 months ago

icecream17 commented 3 months ago

mathbox only. This strengthens mulgt0 to mulgt0b2d, so overall a very minor pr

icecream17 commented 3 months ago

With the hint from https://github.com/metamath/set.mm/pull/3792#issuecomment-1909467443 I found https://math.stackexchange.com/questions/2964961/is-mathbbr-the-only-complete-ordered-abelian-group

So multiplication is commutative if addition is commutative, since we have a complete, ordered, nontrivial, but not necessarily Abelian group.