Commit 2024-10-14 12:17 2ed7908c

View on Github →

chore: unused arguments (#17348)

Estimated changes

modified theorem Finset.card_eq_sum_ones
modified def DirectSum.sigmaLcurry
modified theorem Set.mulIndicator_eq_one
modified theorem pow_eq_zero_of_le
modified theorem Finset.cast_card
modified theorem RCLike.isCauSeq_im
modified theorem RCLike.isCauSeq_re
modified theorem Complex.isCauSeq_re
modified theorem DFinsupp.mapRange_id
modified def fintypeOfFintypeNe
modified theorem NeZero.nat_of_injective
modified theorem Nat.iInf_const_zero
modified theorem Sym2.fromRel_bot
modified theorem Sym2.fromRel_ne
modified theorem Sym2.fromRel_top
modified theorem QuotientGroup.eq_one_iff
modified theorem LinearMap.pi_zero
modified theorem Equiv.subtypeEquiv_refl
modified theorem Function.Injective2.left'
modified theorem Function.const_injective
modified theorem Set.pi_univ_Ioi_subset
modified theorem Derivation.eqOn_adjoin
modified theorem WittVector.mulN_isPoly
modified theorem isCompact_singleton
modified theorem isLindelof_singleton