English
Nonzero scalar multiplication distributes over piAntidiag in a way that selects elements divisible by n componentwise and scales the target sum accordingly.
Русский
Ненулевая кратность на piAntidiag распадается по компонентам так, чтобы выбрать элементы кратные n и масштабировать общую сумму.
LaTeX
$$$n\\cdot \\piAntidiag(s, m) = \\{ f \\in \\piAntidiag(s, n\\cdot m) \\\\mid \\forall i \\in s,\\; n \\mid f(i) \\}$$$
Lean4
theorem nsmul_piAntidiag [DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
n•ℕpiAntidiag s m = {f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} :=
by
ext f
refine mem_smul_finset.trans ?_
simp only [mem_filter, mem_piAntidiag, and_assoc]
constructor
· rintro ⟨f, rfl, hf, rfl⟩
simpa [← mul_sum, hn] using hf
rintro ⟨hfsum, hfsup, hfdvd⟩
have (i : _) : n ∣ f i := by
by_cases hi : i ∈ s
· exact hfdvd _ hi
· rw [not_imp_comm.1 (hfsup _) hi]
exact dvd_zero _
refine ⟨fun i ↦ f i / n, ?_⟩
simp [funext_iff, Nat.mul_div_cancel', ← Nat.sum_div, *]
aesop
