Theorem Setoid.liftFinsuppEquiv_apply_mk

Modification history

2026-10-20 16:41
Mathlib/Data/Finsupp/Quotient.lean
chore(Data/Finsupp/Quotient): automated extraction from #28013 (#45090) …
Added Setoid.liftFinsuppEquiv_apply_mkView on Github →