Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.succ_above_cycle_range

Modification history

2021-04-24 19:36
src/group_theory/perm/fin.lean
feat(linear_algebra): Lagrange formulas for expanding `det` along a row or column (#6897) …
Added fin.succ_above_cycle_rangeView on Github →