mathlib3
8d71ec99 - chore(data/fin): a few more lemmas about `fin.insert_nth` (#5079)

Commit

5 years ago

chore(data/fin): a few more lemmas about `fin.insert_nth` (#5079)

Author

urkud

urkud

Parents

Loading