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)

Estimated changes