Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.support_map_range_of_injective

Modification history

2022-08-19 19:30
src/data/finsupp/basic.lean
refactor(data/finsupp/basic): split `data/finsupp/basic` into three parts (#15699) …
Modified finsupp.support_map_range_of_injectiveView on Github →
2022-04-10 09:05
src/data/finsupp/basic.lean
feat(ring_theory/polynomial/opposites + data/{polynomial/basic + finsupp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162) …
Added finsupp.support_map_range_of_injectiveView on Github →