Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-19 08:19 0a0e8a53

View on Github →

feat(tactic/ext): ext now applies to prod; fix ext on function types (#158)

Estimated changes

Modified analysis/metric_space.lean

Modified analysis/topology/topological_space.lean

Modified data/prod.lean

modified theorem prod.ext

added theorem prod.ext_iff

Modified docs/tactics.md

Modified tactic/basic.lean

Modified tactic/interactive.lean

Modified tests/tactics.lean