Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-04 18:18 fd0cdaee

View on Github →

feat(linear_algebra/pi): pi_option_equiv_prod (#9003)

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.pi_option_equiv_prod

Modified src/linear_algebra/pi.lean

added def linear_equiv.pi_option_equiv_prod