mathlib3

207c9259 - feat(combinatorics/additive/e_transform): e-transforms (#18683)

feat(combinatorics/additive/e_transform): e-transforms (#18683) Define the general e-transform along with two special cases: * The Dyson e-transform, which turns `(s, t)` into `(s ∪ e • t, t ∩ e⁻¹ • s)`. * An pair of unnamed transforms, which turn `(s, t)` into `(s ∩ s • e, t ∪ e⁻¹ • t)` and `(s ∪ s • e, t ∩ e⁻¹ • t)`.