Commit 2025-03-14 22:44 56bfc1e7

View on Github →

chore: unsimp Set.prod_singleton (#22937)

Estimated changes

Modified Mathlib/Data/Set/Prod.lean

modified theorem Set.singleton_prod_singleton

Modified Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

Modified Mathlib/NumberTheory/LSeries/Convolution.lean

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Topology/Algebra/ProperAction/Basic.lean

Modified Mathlib/Topology/CompactOpen.lean

modified theorem ContinuousMap.image_coev