Commit 2025-02-11 10:41 c3090b61

View on Github →

chore: golf theorems using ⊥ = 1 def-eq (#21203) See Zulip for some brief discussion on this def-eq.

Estimated changes

modified theorem bot_eq_one
modified theorem eq_one_or_one_lt
modified theorem le_one_iff_eq_one
modified theorem one_lt_iff_ne_one
modified theorem one_lt_of_ne_one
modified theorem one_not_mem_iff