Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.update_apply_equiv_apply

Modification history

2020-12-01 20:05
src/data/equiv/basic.lean
feat(linear_algebra/multilinear): Add dom_dom_congr (#5136)
Added function.update_apply_equiv_applyView on Github →