Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-02 16:52 12bd22bf

View on Github →

Group morphisms (#30)

  • feat(algebra/group): morphisms and antimorphisms Definitions, image of one and inverses, and computation on a product of more than two elements in big_operators.

Estimated changes

added theorem anti_mph_prod
added theorem inv_prod
added theorem mph_prod
added theorem group_anti_hom.inv
added theorem group_anti_hom.one
added theorem group_hom.inv
added theorem group_hom.one
added def is_group_hom