diff --git a/scripts/nolints.txt b/scripts/nolints.txt index ccb5f9922f946..3551a7d157a1f 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -27,26 +27,10 @@ apply_nolint mul_hom.ext_iff to_additive_doc apply_nolint one_hom.comp_assoc to_additive_doc -- algebra/order/group.lean -apply_nolint inv_le_of_inv_le' to_additive_doc -apply_nolint inv_lt_of_inv_lt' to_additive_doc -apply_nolint inv_mul_lt_of_lt_mul to_additive_doc -apply_nolint inv_of_one_lt_inv to_additive_doc -apply_nolint le_inv_mul_of_mul_le to_additive_doc -apply_nolint le_inv_of_le_inv to_additive_doc -apply_nolint le_one_of_one_le_inv to_additive_doc apply_nolint left.inv_le_one_iff to_additive_doc apply_nolint left.inv_lt_one_iff to_additive_doc apply_nolint left.one_le_inv_iff to_additive_doc apply_nolint left.one_lt_inv_iff to_additive_doc -apply_nolint lt_inv_mul_of_mul_lt to_additive_doc -apply_nolint lt_inv_of_lt_inv to_additive_doc -apply_nolint lt_mul_of_inv_mul_lt to_additive_doc -apply_nolint lt_of_inv_lt_inv to_additive_doc -apply_nolint mul_le_of_le_inv_mul to_additive_doc -apply_nolint mul_lt_of_lt_inv_mul to_additive_doc -apply_nolint one_le_of_inv_le_one to_additive_doc -apply_nolint one_lt_inv_of_inv to_additive_doc -apply_nolint one_lt_of_inv_lt_one to_additive_doc apply_nolint right.inv_le_one_iff to_additive_doc apply_nolint right.one_le_inv_iff to_additive_doc