Commit 2026-07-18 00:01 83a4552f

View on Github →

chore(MathlibTest): fix defLemma warnings (#40593) In all these cases, a dummy definition was declared of type True: the defProp linter complains that a declaration of type True should be a lemma. Instead, change to a definition with value (the natural 0).

Estimated changes