Commit 2025-01-16 11:16 50b66b2e

View on Github →

chore: survey of simp porting notes (#20787) I've removed many porting notes that had resulted from the simpNF linter. I've left in place all porting notes about removing @[simp] but where the proof is rfl or Iff.rfl.

Estimated changes

modified theorem Subgroup.card_bot
modified theorem Finset.empty_mem_powerset
modified theorem Finset.mem_powerset_self
modified theorem Finset.mem_univ_val
modified theorem List.rotate'_nil
modified theorem List.rotate_cons_succ
modified theorem Multiset.mem_ndinsert_self
modified theorem Con.conGen_idem
modified theorem Polynomial.coeff_toSubring'