Commit 2024-01-30 02:26 9cc09f63

View on Github →

chore(WithTop): less abuse of defeq to Option _ (#9986) Also reuse proofs here and there.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

modified theorem WithTop.add_coe_eq_top_iff

modified theorem WithTop.coe_add_eq_top_iff

Modified Mathlib/Order/WithBot.lean

modified theorem WithBot.lt_coe_iff