Mathlib v3 is deprecated. Go to Mathlib v4

Def alternating_map.prod

Modification history

2023-05-27 08:18

src/linear_algebra/alternating.lean

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

Added alternating_map.prod View on Github →