mathlib
340dd69f - fix(*): remove some simp lemmas (#6541)

Commit
4 years ago
fix(*): remove some simp lemmas (#6541) All of these simp lemmas are also declared in core. Maybe one of the copies can be removed in a future PR, but this PR is just to remove the duplicate simp attributes. This is part of fixing linting problems in core, done in leanprover-community/lean#545. Most of the duplicate simp lemmas are fixed in `core`, but I prefer to remove the simp attribute here in mathlib if the simp lemmas were already used in core.
Author
Parents
Loading