Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-08-16 16:19
f8241b74
View on Github →
feat(algebra/big_operators/basic): prod_subsingleton (
#8423
)
Estimated changes
Modified
src/algebra/big_operators/basic.lean
added
theorem
finset.prod_unique_nonempty
added
theorem
fintype.prod_subsingleton
added
theorem
fintype.prod_unique
Modified
src/algebra/group/units.lean
added
theorem
unique_has_one
Modified
src/data/fintype/card.lean
deleted
theorem
fintype.prod_unique