Test: Group Theory

[Charles-Johnson]

Can we express the group property of a given set and operation?

Closure property

let (_s_ with _o_ form a group) => _a_ in _s_ and _b_ in _s_ => _a_ _o_ _b_ in _s_

Inverse and Identity properties

let (_s_ with _o_ form a group) => (_a_ in _s_) => (_i_ exists_such_that) ((_a_ _o_ _i_ -> _a_) and _i_ _o_ _a_ -> _a_) and (_b_ exists_such_that) (_b_ in _s_ and (_a_ _o_ _b_ -> _i_) and _b_ _o_ _a_ -> _i_)

Associativity property

let (_s_ with _o_ form a group) => (_a_ in _s_ and _b_ in _s_ and _c_ in _s_) => _a_ _o_ (_b_ _o_ _c_) = (_a_ _o_ _b_) _o_ _c_

Equality definition

let (_y_ exists_such_that) (_x_ -> _y_ and _z_ -> _y_) => _x_ = _y_

[Charles-Johnson]

I should try to make a tutorial for this