Def Mathlib.Linter.TextBased.UnicodeLinter.othersInMathlib

Modification history

2026-04-13 16:58

Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean

feat(Tactic/Linter): lint unwanted unicode (#36773) …

Added Mathlib.Linter.TextBased.UnicodeLinter.othersInMathlib View on Github →