Commit 2025-03-20 03:52 a54e8f41

View on Github →

chore(Logic/Equiv): split some chunks off large file Equiv/Basic.lean (#23099) This PR tries to clean up Mathlib.Equiv.Basic by splitting off some chunks and moving them to other files:

  • Results focussed on the List type move to the start of Logic.Equiv.List
  • Results focussed on the Option type move to the end of Logic.Equiv.Option
  • Results focussed on product types go to a new file Logic.Equiv.Prod
  • Results focussed on sum types go to a new file Logic.Equiv.Sum

Estimated changes

deleted theorem Equiv.Perm.sumCongr_apply
deleted theorem Equiv.Perm.sumCongr_refl
deleted theorem Equiv.Perm.sumCongr_symm
deleted theorem Equiv.Perm.sumCongr_trans
deleted theorem Equiv.coe_prodComm
deleted theorem Equiv.coe_prodUnique
deleted theorem Equiv.coe_sigmaUnique
deleted theorem Equiv.coe_uniqueProd
deleted def Equiv.curry
deleted def Equiv.emptyProd
deleted def Equiv.emptySum
deleted theorem Equiv.emptySum_apply_inr
deleted def Equiv.funSplitAt
deleted def Equiv.pemptyProd
deleted def Equiv.piSplitAt
deleted def Equiv.pprodCongr
deleted def Equiv.pprodProd
deleted def Equiv.prodAssoc
deleted def Equiv.prodComm
deleted theorem Equiv.prodComm_apply
deleted theorem Equiv.prodComm_symm
deleted def Equiv.prodCongr
deleted def Equiv.prodCongrLeft
deleted theorem Equiv.prodCongrLeft_apply
deleted theorem Equiv.prodCongr_refl_left
deleted theorem Equiv.prodCongr_symm
deleted def Equiv.prodEmpty
deleted def Equiv.prodPEmpty
deleted def Equiv.prodPProd
deleted def Equiv.prodPUnit
deleted def Equiv.prodShear
deleted def Equiv.prodUnique
deleted theorem Equiv.prodUnique_apply
deleted def Equiv.psumCongr
deleted def Equiv.psumEquivSum
deleted def Equiv.psumSum
deleted def Equiv.punitProd
deleted def Equiv.sigmaPUnit
deleted def Equiv.sigmaUnique
deleted theorem Equiv.sigmaUnique_apply
deleted def Equiv.subtypeSum
deleted def Equiv.sumAssoc
deleted theorem Equiv.sumAssoc_apply_inr
deleted def Equiv.sumComm
deleted theorem Equiv.sumComm_symm
deleted def Equiv.sumCompl
deleted theorem Equiv.sumCompl_apply_inl
deleted theorem Equiv.sumCompl_apply_inr
deleted def Equiv.sumCongr
deleted theorem Equiv.sumCongr_refl
deleted theorem Equiv.sumCongr_symm
deleted theorem Equiv.sumCongr_trans
deleted def Equiv.sumEmpty
deleted theorem Equiv.sumEmpty_apply_inl
deleted def Equiv.sumPSum
deleted def Equiv.sumSumSumComm
deleted theorem Equiv.sumSumSumComm_symm
deleted def Equiv.uniqueProd
deleted theorem Equiv.uniqueProd_apply
deleted def Equiv.uniqueSigma
deleted theorem Equiv.uniqueSigma_apply
added theorem Equiv.coe_prodComm
added theorem Equiv.coe_prodUnique
added theorem Equiv.coe_sigmaUnique
added theorem Equiv.coe_uniqueProd
added def Equiv.curry
added def Equiv.emptyProd
added def Equiv.funSplitAt
added def Equiv.pemptyProd
added def Equiv.piSplitAt
added def Equiv.pprodCongr
added def Equiv.pprodProd
added def Equiv.prodAssoc
added def Equiv.prodComm
added theorem Equiv.prodComm_apply
added theorem Equiv.prodComm_symm
added def Equiv.prodCongr
added theorem Equiv.prodCongr_symm
added def Equiv.prodEmpty
added def Equiv.prodPEmpty
added def Equiv.prodPProd
added def Equiv.prodPUnit
added def Equiv.prodShear
added def Equiv.prodUnique
added theorem Equiv.prodUnique_apply
added def Equiv.punitProd
added def Equiv.sigmaPUnit
added def Equiv.uniqueProd
added theorem Equiv.uniqueProd_apply
added def Equiv.emptySum
added def Equiv.psumCongr
added def Equiv.psumSum
added def Equiv.subtypeSum
added def Equiv.sumAssoc
added def Equiv.sumComm
added theorem Equiv.sumComm_symm
added def Equiv.sumCompl
added def Equiv.sumCongr
added theorem Equiv.sumCongr_refl
added theorem Equiv.sumCongr_symm
added theorem Equiv.sumCongr_trans
added def Equiv.sumEmpty
added def Equiv.sumPSum