Commit 2024-11-28 14:24 cbd40933
View on Github →feat: {a, b} * s = a • s ∪ b • s
(#19406)
and other simple pointwise lemmas.
From GrowthInGroups (LeanCamCombi)
feat: {a, b} * s = a • s ∪ b • s
(#19406)
and other simple pointwise lemmas.
From GrowthInGroups (LeanCamCombi)