English
Let R be a commutative ring, M and N be R-modules, and ι, κ finite sets. For a bijection e: κ ≃ ι and families m: ι → M, n: ι → N, the vanishing of the composed families is equivalent to the vanishing of the original families: VanishesTrivially_R(m ∘ e, n ∘ e) iff VanishesTrivially_R(m, n).
Русский
Пусть R — коммутативное кольцо, M и N — модулей над R, ι и κ — конечные множества. Пусть e: κ ≃ ι — биекция, m: ι → M и n: ι → N. Тогда исчезновение тривиальным образом сохраняется под композициями с эквивалентом: VanishesTrivially_R(m ∘ e, n ∘ e) ⇔ VanishesTrivially_R(m, n).
LaTeX
$$$ \\text{VanishesTrivially}_R(m \\circ e, n \\circ e) \\iff \\text{VanishesTrivially}_R(m, n) $$$
Lean4
theorem _root_.Equiv.vanishesTrivially_comp {κ} [Fintype κ] (e : κ ≃ ι) :
VanishesTrivially R (m ∘ e) (n ∘ e) ↔ VanishesTrivially R m n := by
simp [VanishesTrivially, ← e.forall_congr_right, ← (e.arrowCongr (.refl _)).exists_congr_right, ← e.sum_comp]
