Commit 2025-01-03 17:09 fbe1f6b0

View on Github →

feat: add sumPiEquivProdPi and piUnique (#20195) From FLT. Add topological and algebraic versions of Equiv.sumPiEquivProdPi and Equiv.piUnique.

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

added def LinearEquiv.piUnique

added def LinearEquiv.sumPiEquivProdPi

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added def ContinuousLinearEquiv.piCongrLeft

added def ContinuousLinearEquiv.piUnique

added def ContinuousLinearEquiv.sumPiEquivProdPi

Modified Mathlib/Topology/Basic.lean

added theorem Equiv.continuous_symm_iff

added theorem Equiv.isOpenMap_symm_iff

Modified Mathlib/Topology/Homeomorph.lean

added def Homeomorph.piUnique

added def Homeomorph.sumPiEquivProdPi