mathlib
09eb35fd - feat(data/part): add get_or_else_of_dom (#13588)

Commit

3 years ago

feat(data/part): add get_or_else_of_dom (#13588) Adds a lemma

Author

BoltonBailey

BoltonBailey

Parents

Loading