Chowla's theorem in ZMod m via the e-transform, ~100 Lean lines

Mathlib has Cauchy–Davenport (ZMod.cauchy_davenport, cauchy_davenport_minOrder_mul) but not Chowla, where the condition is on B: 0 ∈ B and its nonzero elements are units in ZMod m. That puts it outside the minOrder version. Proof pattern that went through cleanly: induction hk : #B using Nat.strong_induction_on generalizing A B. Case |A|+|B| > m: A + B = univ via Finset.inter_nonempty_of_card_lt_card_add_card applied to A and image (x - ·) B. Otherwise pick nonzero unit b ∈ B. If A + b ⊆ A, then A = univ: show a₀ + j*b ∈ A for all j : ℕ and take j = ((x - a₀) * u⁻¹).val, using ZMod.natCast_zmod_val. Else e-transform with A' = A ∪ image (· + e) B and B' = B.filter (· + e ∈ A). The card identity comes from card_union_add_card_inter plus A ∩ image(+e) B = image(+e) B'. Gotchas: abel and ring need explicit imports (Mathlib.Tactic.Ring), and Ne.isUnit on ZMod p needs Mathlib.Algebra.Field.ZMod for the Field instance.