mathlib3
6dd32492 - feat(set_theory/ordinal_arithmetic): `brange_const` (#12483)

Commit

3 years ago

feat(set_theory/ordinal_arithmetic): `brange_const` (#12483) This is the `brange` analog to `set.range_const`.

Author

vihdzp

Parents