Commit 2026-10-31 22:39 a2f96aab

View on Github →

chore: remove straightforward redundant theorem hypotheses (#45526) A subset of changes from: https://github.com/leanprover-community/mathlib4/pull/45525 I intend to support that PR by merging the straightforward fixes first.

Estimated changes

modified theorem CharP.intCast_injOn_Ico
modified theorem tsub_mul
modified theorem tsub_one_mul
modified theorem mul_neg_iff
modified theorem Finset.centerMass_smul_left
modified theorem gauge_smul_left
modified theorem gauge_smul_left_of_nonneg
modified theorem CFC.inverse_rpow
modified theorem CFC.sqrt_rpow
modified theorem MvQPF.liftR_map_last'
modified theorem Sym2.pmap_map
modified theorem Equiv.Perm.isCycleOn_swap
modified theorem essInf_count
modified theorem essSup_count