Def Equiv.sigmaEquivProd

Modification history

2025-08-22 13:19
Mathlib/Logic/Equiv/Defs.lean
feat: grind annotations in Logic/Equiv/Defs (#28025)
Modified Equiv.sigmaEquivProdView on Github →
2023-08-10 19:52
Mathlib/Logic/Equiv/Defs.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified Equiv.sigmaEquivProdView on Github →
2023-07-03 14:48
Mathlib/Logic/Equiv/Defs.lean
refactor: move all `register_simp_attr`s to 1 file (#5681) …
Modified Equiv.sigmaEquivProdView on Github →
2022-11-20 06:21
Mathlib/Logic/Equiv/Defs.lean
fix(Tactic/Simps): use capital letter for namespace (#647) …
Modified Equiv.sigmaEquivProdView on Github →
2022-11-18 00:38
Mathlib/Logic/Equiv/Defs.lean
feat: port logic.equiv.defs (#550) …
Added Equiv.sigmaEquivProdView on Github →