Theorem Prod.mul_def

Modification history

2025-03-10 06:24

Mathlib/Algebra/Group/Prod.lean

chore(Algebra/Group/Prod): move notation to a new file (#22567)

Modified Prod.mul_def View on Github →

2022-12-13 13:20

Mathlib/Algebra/Group/Prod.lean

feat: port Algebra.Group.Prod (#968) …

Added Prod.mul_def View on Github →