Theorem Tactic.Elementwise.forget_hom_Type

Modification history

2026-02-13 16:28
Mathlib/Tactic/CategoryTheory/Elementwise.lean
chore: add missing `namespace`s (#34631) …
Deleted Tactic.Elementwise.forget_hom_TypeView on Github →
2024-01-17 23:23
Mathlib/Tactic/CategoryTheory/Elementwise.lean
chore(*): rename `FunLike` to `DFunLike` (#9785) …
Modified Tactic.Elementwise.forget_hom_TypeView on Github →
2023-06-17 07:00
Mathlib/Tactic/CategoryTheory/Elementwise.lean
chore: have CI run on tests in subdirectories (#5065) …
Modified Tactic.Elementwise.forget_hom_TypeView on Github →
2023-03-16 04:49
Mathlib/Tactic/Elementwise.lean
feat: port `@[elementwise]` attribute (#2882) …
Added Tactic.Elementwise.forget_hom_TypeView on Github →