mathlib3
206673e7 - chore(*): trivial golfing using dec_trivial tactic (#3949)

Commit

5 years ago

chore(*): trivial golfing using dec_trivial tactic (#3949)

References

#4925 - Make prime-avoidance branch build

Author

jcommelin

jcommelin

Parents

Loading