Commit 2022-06-04 15:25 cfcc3a1b

View on Github →

chore(data/finsupp/basic): make arguments explicit (#14551) This follow the pattern that arguments to an = lemma should be explicit if they're not implied by other arguments.

Estimated changes

Modified src/algebra/monoid_algebra/grading.lean

Modified src/data/finsupp/basic.lean

modified theorem finsupp.single_add

modified theorem finsupp.single_eq_pi_single

modified theorem finsupp.single_eq_update

modified theorem finsupp.single_neg

modified theorem finsupp.single_sub

modified theorem finsupp.single_zero

modified theorem finsupp.support_single_ne_zero

Modified src/data/finsupp/multiset.lean

Modified src/data/mv_polynomial/basic.lean

modified theorem mv_polynomial.C_add

Modified src/data/mv_polynomial/variables.lean

Modified src/data/polynomial/basic.lean

Modified src/group_theory/free_abelian_group_finsupp.lean

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/std_basis.lean

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/polynomial/homogeneous.lean

Modified src/ring_theory/polynomial/symmetric.lean