Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-24 19:58 fb878e78

View on Github →

feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol (#2038)

Estimated changes

Modified docs/commands.md

Modified src/algebra/field.lean

modified theorem is_ring_hom.map_div

modified theorem is_ring_hom.map_inv

Modified src/algebra/module.lean

modified theorem is_linear_map.map_add

modified theorem is_linear_map.map_neg

modified theorem is_linear_map.map_sub

modified theorem is_linear_map.map_zero

Modified src/data/list/basic.lean

modified theorem list.find_some

Modified src/tactic/lint.lean

Created test/lint_simp_var_head.lean