Theorem Finset.isSquare_prod

Modification history

2025-07-05 03:31

Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean

chore(Algebra/BigOperators): rename variables away from greek letters (#26521) …

Modified Finset.isSquare_prod View on Github →

2025-04-10 03:41

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

chore: split `Algebra.BigOperators.Group.Finset.Basic` (#23897) …

Modified Finset.isSquare_prod View on Github →

2024-07-16 20:24

Mathlib/Algebra/BigOperators/Group/Finset.lean

feat(Algebra/BigOperators/Group/Finset): Lemma for product being a square (#14622) …

Added Finset.isSquare_prod View on Github →