Commit 2026-04-27 10:44 a45b1dba
View on Github →feat(Order): add sdiff_left_inj, rename eq_of_sdiff_eq_sdiff (#38371)
Rename eq_of_sdiff_eq_sdiff (GeneralizedBooleanAlgebra) to sdiff_right_inj,
reflecting that the common fixed element is the left operand of \. A @[deprecated]
alias preserves the old name.
Add the companion sdiff_left_inj in GeneralizedCoheytingAlgebra
(Mathlib/Order/Heyting/Basic.lean), where the fixed element is the right operand of \.
The proof is a 1-line consequence of sdiff_sup_cancel. Since GCA ⊂ GBA, this applies
everywhere eq_of_sdiff_left_eq does and strictly more.
The _left/_right convention matches add_left_cancel/add_right_cancel: the suffix
names the position of the common/fixed element.
Moves:
eq_of_sdiff_eq_sdiff→sdiff_right_inj