Commit 2024-03-24 09:17 acda20c6

View on Github →

style: remove redundant instance arguments (#11581) I removed some redundant instance arguments throughout Mathlib. To do this, I used VS Code's regex search. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/repeating.20instances.20from.20variable.20command I closed the previous PR for this and reopened it.

Estimated changes

modified theorem Fintype.prod_fiberwise'
modified theorem Fintype.prod_fiberwise
modified theorem MonoidHom.comp_mul
modified theorem IsUnit.exists_left_inv
modified theorem pow_two_semiclosed
modified theorem WithBot.unbot_one
modified theorem StarAlgHom.map_adjoin
modified theorem mul_bit1
modified theorem Matrix.scalar_commute
modified theorem Matrix.scalar_commute_iff
modified theorem Multiset.erase_attach_map
modified theorem Monoid.one_lt_exponent
modified theorem IsFreeGroup.ofMulEquiv
modified theorem rank_pos
modified theorem rank_zero_iff_forall_zero
modified theorem Module.equiv
modified theorem isGLB_prod
modified theorem isLUB_prod
modified def RingHom.kerLift
modified theorem RingHom.kerLift_injective
modified theorem RingHom.kerLift_mk
modified def Algebra.intNormAux
modified theorem atBot_atTop_le_cocompact
modified theorem atBot_le_cocompact
modified theorem atTop_le_cocompact
modified theorem cocompact_eq_atBot
modified theorem cocompact_eq_atBot_atTop
modified theorem cocompact_eq_atTop
modified theorem cocompact_le_atBot
modified theorem cocompact_le_atBot_atTop
modified theorem cocompact_le_atTop
modified theorem closure_induced
modified theorem continuous_discrete_rng
modified theorem isClosed_induced_iff'