Commit 2024-08-28 16:23 22246afc

View on Github →

chore: make two arguments of Finsupp.total implicit (#16221) See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Finsupp.2Etotal.

Estimated changes

modified theorem Basis.coe_repr_symm
modified theorem Basis.repr_symm_apply
modified theorem Basis.repr_total
modified theorem Basis.total_repr
modified theorem Module.DualBases.lc_def
modified theorem Finsupp.range_total
modified theorem Finsupp.span_eq_range_total
modified theorem Finsupp.total_apply
modified theorem Finsupp.total_fin_zero
modified theorem Finsupp.total_range
modified theorem Finsupp.total_single
modified theorem Finsupp.total_unique
modified theorem Finsupp.total_zero
modified theorem Finsupp.total_zero_apply