mathlib3
8ec447d8 - fix(*): remove `@[nolint simp_nf]` (#2450)

Commit
5 years ago
fix(*): remove `@[nolint simp_nf]` (#2450) This removes a couple more nolints: - `coe_units_equiv_ne_zero` doesn't cause any problems anymore - `coe_mk` is redundant - `mk_eq_div` was not in simp-normal form (previously the linter timed out instead of reporting it as an error) - `factor_set.coe_add` is redundant
Author
Parents
Loading