fin): The equivalence between `fin n → fin m` and `fin (m ^ n)` (#14817)

Commit

2 years ago

feat(algebra/big_operators/fin): The equivalence between `fin n → fin m` and `fin (m ^ n)` (#14817) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

YaelDillies

Parents

178a3265

mathlib3 cdb01be3 - feat(algebra/big_operators/fin): The equivalence between `fin n → fin m` and `fin (m ^ n)` (#14817)

mathlib3
cdb01be3 - feat(algebra/big_operators/fin): The equivalence between `fin n → fin m` and `fin (m ^ n)` (#14817)