Theorem imp_trans'

Modification history

2025-06-14 00:25
Mathlib/Tactic/GCongr/CoreAttrs.lean
feat(gcongr): fix pattern elaborator and @[gcongr] for lemmas introducing binders (#25716) …
Deleted imp_trans'View on Github →
2025-06-10 22:11
Mathlib/Tactic/GCongr/CoreAttrs.lean
feat: let `gcongr` deal with implications (#25534) …
Added imp_trans'View on Github →