mathlib
58d97787
- chore(set_theory/ordinal/arithmetic): clean up `is_normal.sup` and related (#15162)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(set_theory/ordinal/arithmetic): clean up `is_normal.sup` and related (#15162) We golf various theorems and tweak their arguments. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
vihdzp
Parents
8cfa8363
Loading