Lax Lean Archive

Proof of `Linearly-finite and recognisable series` (2nd statement)

groundedproofs/Lax619925Proofs/Recognisable.lean · lax-619925

What this proof establishes

no assumptions

thm✓Lax619925.Recognisable (2nd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The class of linearly finite series is closed under addition, scalar multiplication, and left derivatives (paper §4). Each operation is witnessed by an explicit finite generator set: addition uses G∪HG ∪ H, while scalar multiplication and left derivatives reuse the original generators.