basic): correct the name of `finset.range_coe` which does not mention coercions (#18052)

Commit

2 years ago

fix(data/finset/basic): correct the name of `finset.range_coe` which does not mention coercions (#18052) This also adds the missing lemma that should have had that name.

Author

eric-wieser

Parents

5a3e8195

mathlib3 43a289b5 - fix(data/finset/basic): correct the name of `finset.range_coe` which does not mention coercions (#18052)

mathlib3
43a289b5 - fix(data/finset/basic): correct the name of `finset.range_coe` which does not mention coercions (#18052)