Revision #3023 → #3245 · back to history
modifiedFunctionb2a7701b9cc0
| Field | From #3023 | To #3245 |
|---|
| mathlib.decl | Function | — |
| note | Functions `α → β` are a primitive notion in Lean's type theory used throughout Mathlib. | Functions `α → β` are a primitive notion in Lean's type theory used throughout Mathlib. (Cited declaration no longer exists in Mathlib — cleared by the decl-existence sweep.) |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedIndexed familybabb27a93d8f
| Field | From #3023 | To #3245 |
|---|
| mathlib.decl | Function | — |
| note | Indexed families are represented as ordinary functions `ι → X` in Lean; no separate definition is needed. | Indexed families are represented as ordinary functions `ι → X` in Lean; no separate definition is needed. (Cited declaration no longer exists in Mathlib — cleared by the decl-existence sweep.) |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |