Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#16179)
Browse files Browse the repository at this point in the history
I am happy to remove some nolints for you!
  • Loading branch information
leanprover-community-bot committed Aug 21, 2022
1 parent ec73f6e commit b46c895
Showing 1 changed file with 0 additions and 31 deletions.
31 changes: 0 additions & 31 deletions scripts/nolints.txt
Expand Up @@ -452,37 +452,6 @@ apply_nolint stream.is_bisimulation doc_blame
apply_nolint add_action.minimal_period_pos fintype_finite
apply_nolint mul_action.minimal_period_pos fintype_finite

-- field_theory/finite/basic.lean
apply_nolint finite_field.exists_nonsquare fintype_finite
apply_nolint finite_field.is_square_of_char_two fintype_finite

-- field_theory/finite/galois_field.lean
apply_nolint galois_field.is_galois fintype_finite

-- field_theory/finite/polynomial.lean
apply_nolint mv_polynomial.R.finite_dimensional fintype_finite
apply_nolint mv_polynomial.eq_zero_of_eval_eq_zero fintype_finite
apply_nolint mv_polynomial.ker_evalₗ fintype_finite
apply_nolint mv_polynomial.map_restrict_dom_evalₗ fintype_finite
apply_nolint mv_polynomial.range_evalᵢ fintype_finite

-- field_theory/finite/trace.lean
apply_nolint finite_field.trace_to_zmod_nondegenerate fintype_finite

-- field_theory/fixed.lean
apply_nolint fixed_points.finite_dimensional fintype_finite
apply_nolint fixed_points.is_integral fintype_finite
apply_nolint fixed_points.normal fintype_finite
apply_nolint fixed_points.separable fintype_finite
apply_nolint fixed_points.to_alg_hom_bijective fintype_finite

-- field_theory/galois.lean
apply_nolint is_galois.of_fixed_field fintype_finite

-- field_theory/primitive_element.lean
apply_nolint field.exists_primitive_element_of_fintype_bot fintype_finite
apply_nolint field.exists_primitive_element_of_fintype_top fintype_finite

-- geometry/euclidean/circumcenter.lean
apply_nolint affine_independent.exists_unique_dist_eq fintype_finite

Expand Down

0 comments on commit b46c895

Please sign in to comment.