Commit 2023-07-16 13:05 48029e81

View on Github →

chore: forward-port leanprover-community/mathlib#19234 (#5887)

Estimated changes

Modified Mathlib/Algebra/Group/Prod.lean

added def MulEquiv.prodProdProdComm

added theorem MulEquiv.prodProdProdComm_symm

added theorem MulEquiv.prodProdProdComm_toEquiv

Modified Mathlib/Algebra/Ring/Prod.lean

added def RingEquiv.prodProdProdComm

added theorem RingEquiv.prodProdProdComm_symm

added theorem RingEquiv.prodProdProdComm_toAddEquiv

added theorem RingEquiv.prodProdProdComm_toEquiv

added theorem RingEquiv.prodProdProdComm_toMulEquiv

Modified Mathlib/LinearAlgebra/Prod.lean

added def LinearEquiv.prodProdProdComm

added theorem LinearEquiv.prodProdProdComm_symm

added theorem LinearEquiv.prodProdProdComm_toAddEquiv

Modified Mathlib/Logic/Equiv/Basic.lean

added def Equiv.prodProdProdComm

added theorem Equiv.prodProdProdComm_symm