pointwise): Singleton arithmetic (#15435)

Commit

3 years ago

feat(data/finset/pointwise): Singleton arithmetic (#15435) Lemmas about pointwise operations with a singleton. Also make `s` explicit in `finset.card_inv`.

Author

YaelDillies

Parents

87861dd7

mathlib3 0fc357f5 - feat(data/finset/pointwise): Singleton arithmetic (#15435)

mathlib3
0fc357f5 - feat(data/finset/pointwise): Singleton arithmetic (#15435)