finite): set priority for fintype_insert' and document (#14363)

Commit

3 years ago

feat(data/set/finite): set priority for fintype_insert' and document (#14363) This follows up with some review comments for #14136.

Author

kmill

Parents