Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 13:16 a65de994

View on Github →

feat(data/equiv): Add congr_arg, congr_fun, and ext_iff lemmas to equivs (#5367) These members already exist on the corresponding homs

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_equiv.ext_iff

Modified src/algebra/module/linear_map.lean

added theorem linear_equiv.ext_iff

Modified src/data/equiv/basic.lean

Modified src/data/equiv/mul_add.lean

added theorem mul_equiv.ext_iff

Modified src/data/equiv/ring.lean

added theorem ring_equiv.ext_iff