Mathlib v3 is deprecated. Go to Mathlib v4

Theorem punit.ext

Modification history

2020-07-28 15:30

src/tactic/ext.lean

feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562) …

Added punit.ext View on Github →