mathlib3

e830348b - feat(set_theory/ordinal_arithmetic): Families of ordinals (#11278)

feat(set_theory/ordinal_arithmetic): Families of ordinals (#11278) This PR introduces some API to convert from `ι → β` indexed families to `Π o < b, β` indexed families. This simplifies and contextualizes some existing results.