Commit 2024-01-16 21:01 ef9852fc

View on Github →

feat(Function/Conjugate): add Semiconj.inverse_left (#9724)

  • Add Function.semiconj_iff_comp_eq and Function.Semiconj.inverse_left.
  • Swap arguments of Function.Semiconj.comp_left. The old version is available as Function.Semiconj.trans.
  • Add docstrings.

Estimated changes

modified theorem Function.Commute.id_right
modified theorem Function.Commute.refl
modified theorem Function.Commute.symm
modified theorem Function.Semiconj.comp_left
modified theorem Function.Semiconj.id_left
modified theorem Function.Semiconj.id_right