mathlib3
dfdb38ab - feat(data/fin): nontrivial instance (#3979)

Commit

5 years ago

feat(data/fin): nontrivial instance (#3979) Add an instance `nontrivial (fin (n + 2))`.

References

Author

jsm28

Parents