mathlib3
bc65b7cd - feat(data/list/basic): add `list.range_map` (#13777)

Commit
3 years ago
feat(data/list/basic): add `list.range_map` (#13777) * add `list.range_map` and `list.range_map_coe`; * add `submonoid.closure_eq_image_prod` and `add_submonoid.closure_eq_image_prod`.
Author
Parents
Loading