Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-27 08:18 78fdf68d

View on Github →

feat(linear_algebra/alternating): add 3 missing definitions (#19069)

Estimated changes

Modified src/linear_algebra/alternating.lean

added theorem alternating_map.coe_pi

added theorem alternating_map.coe_prod

added theorem alternating_map.coe_smul_right

added def alternating_map.pi

added def alternating_map.prod

added def alternating_map.smul_right

added theorem linear_map.smul_right_eq_comp

Modified src/linear_algebra/multilinear/basic.lean

modified def multilinear_map.prod