Commit 2022-11-06 08:48 728737c2

View on Github →

feat: port Logic.Function.Conjugate (#533) This is my first PR to mathlib4. It seems to be a short and simple file, but could you please check I got the naming conventions right, please? (in particular: is it Semiconj or SemiConj?) No name changes from mathlib3port, only had to adapt some proofs: e.g. function.comp_app is now Function.comp_apply. Does this need an #align statement, too?

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Init/Function.lean

Created Mathlib/Logic/Function/Conjugate.lean

added theorem Function.Commute.comp_left

added theorem Function.Commute.comp_right

added theorem Function.Commute.id_left

added theorem Function.Commute.id_right

added theorem Function.Commute.option_map

added theorem Function.Commute.refl

added theorem Function.Commute.symm

added def Function.Commute

added theorem Function.Semiconj.commute

added theorem Function.Semiconj.comp_left

added theorem Function.Semiconj.comp_right

added theorem Function.Semiconj.id_left

added theorem Function.Semiconj.id_right

added theorem Function.Semiconj.inverses_right

added theorem Function.Semiconj.option_map

added def Function.Semiconj

added theorem Function.Semiconj₂.comp

added theorem Function.Semiconj₂.id_left

added theorem Function.Semiconj₂.is_associative_left

added theorem Function.Semiconj₂.is_associative_right

added theorem Function.Semiconj₂.is_idempotent_left

added theorem Function.Semiconj₂.is_idempotent_right

added def Function.Semiconj₂