mathlib
7a02c9e6 - fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from `CNF_rec` (#12680)

Commit

3 years ago

fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from `CNF_rec` (#12680) The hypothesis in question was a theorem that could be deduced.

Author

vihdzp

Parents

a3b39c6e

mathlib 7a02c9e6 - fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from `CNF_rec` (#12680)

mathlib
7a02c9e6 - fix(set_theory/ordinal_arithmetic): remove redundant hypothesis from `CNF_rec` (#12680)