Kim Morrison db354d2cde chore: run Batteries linter on Lean (#6364) ... This PR makes fixes suggested by the Batteries environment linters, particularly `simpNF`, and `unusedHavesSuffices`.		2024-12-13 01:28:53 +00:00
..
Basic.lean	doc: adjust file reference in Data.Sum (#6158)	2024-11-21 21:48:27 +00:00
Lemmas.lean	chore: run Batteries linter on Lean (#6364)	2024-12-13 01:28:53 +00:00