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_transView on Github →
2025-06-10 22:11
Mathlib/Tactic/GCongr/CoreAttrs.lean
feat: let `gcongr` deal with implications (#25534) …
Added imp_transView on Github →