Diff — Klein four-group

Revision #2113 → #2853 · back to history

addedEach element is self-inversec451b50ca12b

addedDirect product Z₂ × Z₂55bf99889b9e

addedFundamental Theorem of Finitely Generated Abelian Groups8670b60629b1

modifiedNon-identity elements have order 241ad88eb2b41

Field	From #2113	To #2853
note	`IsKleinFour.mul_self` proves `x * x = 1` for every element; the field `exponent_two` records the same fact.	`IsKleinFour.mul_self` proves `x * x = 1` for every element; the field `IsKleinFour.exponent_two` records the same fact.