mathlib
9a30f8cf - refactor(data/fin): drop `fin.cast_add_right` (#9371)

Commit

4 years ago

refactor(data/fin): drop `fin.cast_add_right` (#9371) This was a duplicate of `fin.nat_add`. Also simplify some definitions of equivalences.

Author

urkud

Parents