Commit 2022-11-26 16:48 0d2f0621

View on Github →

feat: port algebra.group.semiconj (#717) mathlib SHA e50b8c261b0a000b806ec0e1356b41945eda61f7 This completes an earlier partial port of the file. ~~I added a workaround for the issue explained by Floris at https://github.com/leanprover-community/mathlib4/pull/707#issuecomment-1326669750.~~

Estimated changes

Modified Mathlib/Algebra/Group/Semiconj.lean

added theorem SemiconjBy.conj_mk

added theorem SemiconjBy.inv_inv_symm

added theorem SemiconjBy.inv_inv_symm_iff

added theorem SemiconjBy.inv_right

added theorem SemiconjBy.inv_right_iff

added theorem SemiconjBy.inv_symm_left

added theorem SemiconjBy.inv_symm_left_iff

added theorem SemiconjBy.units_coe

added theorem SemiconjBy.units_coe_iff

added theorem SemiconjBy.units_inv_right

added theorem SemiconjBy.units_inv_right_iff

added theorem SemiconjBy.units_inv_symm_left

added theorem SemiconjBy.units_inv_symm_left_iff

added theorem SemiconjBy.units_of_coe

modified def SemiconjBy

added theorem Units.mk_semiconjBy

added theorem semiconjBy_iff_eq

Modified Mathlib/Logic/Function/Basic.lean