Revision #1559 → #2670 · back to history
modifiedNatural numbers form an infinite sete0e7642859a4
| Field | From #1559 | To #2670 |
|---|
| mathlib.decl | Nat.instInfinite | instInfiniteNat |
| provenance | ai | ai-moderated |
modifiedDisjoint union is the coproduct in Set09c422b08e05
| Field | From #1559 | To #2670 |
|---|
| mathlib.decl | CategoryTheory.Types.binaryCoproductColimit | CategoryTheory.Limits.Types.binaryCoproductColimit |
| provenance | ai | ai-moderated |
modifiedForgetting-indices map is bijective iff pairwise disjointb1632512af76
| Field | From #1559 | To #2670 |
|---|
| mathlib.decl | Set.iUnion_eq_sigma_of_disjoint | Set.unionEqSigmaOfDisjoint |
| provenance | ai | ai-moderated |
modifiedEvery vector space has a basis2d518bee344c
| Field | From #1559 | To #2670 |
|---|
| mathlib.decl | Basis.ofVectorSpace | Module.Basis.ofVectorSpace |
| provenance | ai | ai-moderated |