chore(scripts): update nolints.txt (#18357)

I am happy to remove some nolints for you!
leanprover-community · Feb 2, 2023 · 4ef778c · 4ef778c
1 parent d90e4e1
commit 4ef778c
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -342,9 +342,6 @@ apply_nolint stream.is_bisimulation doc_blame
 -- group_theory/group_action/sub_mul_action.lean
 apply_nolint sub_mul_action.has_zero fails_quickly
 
--- linear_algebra/affine_space/basis.lean
-apply_nolint affine_basis.ext_elem fintype_finite
-
 -- linear_algebra/affine_space/matrix.lean
 apply_nolint affine_basis.affine_independent_of_to_matrix_right_inv fintype_finite
 apply_nolint affine_basis.affine_span_eq_top_of_to_matrix_left_inv fintype_finite