Def Mathlib.Linter.AuxLemma.auxLemmaLinter

Modification history

2026-05-28 11:17
Mathlib/Tactic/Linter/AuxLemma.lean
feat(Tactic/Linter): add `auxLemma` linter for auto-generated declaration references (#37364) …
Added Mathlib.Linter.AuxLemma.auxLemmaLinterView on Github →