fix: add @[expose] to make definitions visible across modules

Lean 4.30's module system makes definitions unexposed by default.
`@[expose] public section` is needed for definitions like
IsShiftEquivariant to be unfoldable by tactics and term-mode
unification across module boundaries.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: RaggedR

Mathlib/RingTheory/HopfAlgebra/AscPochhammer.lean

@@ -34,6 +34,8 @@ of the backward difference operator `∇f(x) = f(x) - f(x-1)`.
 * Langer, R., *Determinantal bases and the symmetric group*, arXiv:0907.3950, §1.2.2
 -/
 
+@[expose] public section
+
 noncomputable section
 
 open Polynomial Finset

Mathlib/RingTheory/HopfAlgebra/DeltaOperator.lean

@@ -55,7 +55,7 @@ that these are exactly the sequences of binomial type.
   JMAA 42 (1973)
 -/
 
-public section
+@[expose] public section
 
 noncomputable section
 
@@ -141,7 +141,7 @@ end -- end CommSemiring noncomputable section
 
 /-! ### Forward difference operator (requires subtraction) -/
 
-public section
+@[expose] public section
 
 noncomputable section
 

Mathlib/RingTheory/HopfAlgebra/Lah.lean

@@ -33,6 +33,8 @@ coefficients of `(mk 1)ᵏ = (1-X)⁻ᵏ`.
 * Langer, R., *Determinantal bases and the symmetric group*, arXiv:0907.3950, §1.2.2
 -/
 
+@[expose] public section
+
 noncomputable section
 
 open PowerSeries