Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#15776)
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 Jul 31, 2022
1 parent a574fbe commit bff2f20
Showing 1 changed file with 1 addition and 8 deletions.
9 changes: 1 addition & 8 deletions scripts/nolints.txt
Expand Up @@ -697,13 +697,6 @@ apply_nolint pow_gcd_card_eq_one_iff to_additive_doc
apply_nolint powers_eq_zpowers fintype_finite
apply_nolint subgroup.pow_index_mem fintype_finite

-- group_theory/p_group.lean
apply_nolint is_p_group.bot_lt_center fintype_finite
apply_nolint is_p_group.center_nontrivial fintype_finite
apply_nolint is_p_group.exists_fixed_point_of_prime_dvd_card_of_fixed_point fintype_finite
apply_nolint is_p_group.index fintype_finite
apply_nolint is_p_group.nonempty_fixed_point_of_prime_not_dvd_card fintype_finite

-- group_theory/perm/cycle/basic.lean
apply_nolint equiv.perm.closure_is_cycle fintype_finite
apply_nolint equiv.perm.cycle_induction_on fintype_finite
Expand Down Expand Up @@ -1629,4 +1622,4 @@ apply_nolint Cauchy.gen doc_blame
apply_nolint uniform_space.completion.completion_separation_quotient_equiv doc_blame
apply_nolint uniform_space.completion.cpkg doc_blame
apply_nolint uniform_space.completion.extension₂ doc_blame
apply_nolint uniform_space.completion.map₂ doc_blame
apply_nolint uniform_space.completion.map₂ doc_blame

0 comments on commit bff2f20

Please sign in to comment.