Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.Pi_congr_left'_update

Modification history

2021-12-31 16:13
src/data/equiv/basic.lean
feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474) …
Added function.Pi_congr_left'_updateView on Github →