Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.prod_eq_single_of_mem

Modification history

2021-03-27 03:05
src/algebra/big_operators/basic.lean
feat(algebra/big_operators/basic): add lemmas for a product with two non one factors (#6826) …
Added finset.prod_eq_single_of_memView on Github →