mathlib

7b825f2a - feat(linear_algebra/alternating): Add comp_alternating_map and lemmas (#5476)