Commit 2023-12-04 18:10 f26f1d91

View on Github →

feat(Algebra/Group): lemmas about Commute (#8756)

Estimated changes

added theorem Commute.pi
added theorem Pi.commute_iff
added theorem Pi.semiconjBy_iff
added theorem SemiconjBy.pi
added theorem Commute.prod
added theorem Prod.commute_iff
added theorem Prod.semiconjBy_iff
added theorem SemiconjBy.prod