mathlib3
c235c612 - refactor(set_theory/ordinal_arithmetic): Simpler `bsup` definition (#11386)

Commit

3 years ago

refactor(set_theory/ordinal_arithmetic): Simpler `bsup` definition (#11386) We also simplify some existing proofs.

Author

vihdzp

Parents