Revision #3310 → #3913 · back to history
modifiedCartesian product of n setsbfd8c5ca88c1
| Field | From #3310 | To #3913 |
|---|
| mathlib.decl | Set.prod | Set.pi |
| note | `Set.prod` provides binary Cartesian product of sets; `Set.pi` provides the n-ary version. | `Set.pi` provides the n-ary Cartesian product of sets; `Set.prod` provides the binary version. |
| provenance | ai | ai-moderated |
modifiedFiber of a point46e51dd712df
| Field | From #3310 | To #3913 |
|---|
| mathlib.match_kind | exact | special_case |
| provenance | ai | ai-moderated |
modifiedAnalytic continuationcf729b77b16c
| Field | From #3310 | To #3913 |
|---|
| status | formalized | partial |
addedConstant functionb07722aa17f6
addedReciprocal function 1/x95043e567c9e
addedPreimage properties (image/preimage identities)8796e1edee27