mathlib3
c914e8f5 - refactor(data/fin): define neg like sub (#7408)

Commit
4 years ago
refactor(data/fin): define neg like sub (#7408) Define negation on fin in the same way as subtraction, i.e., using nat.mod (instead of computing it in the integers).
Author
Parents
Loading