mathlib

b35461b8 - feat(logic/basic): `function.mt` and `function.mtr` (#16315)

feat(logic/basic): `function.mt` and `function.mtr` (#16315) Add modus tollens and reversed modus tollens to the `function` namespace so that they are available for dot notation on implications.