of_fintype — Mathlib

English

Given a finite κ and sequences a, y with hay and ham as in the statement, one can construct a VanishesTrivially object from f, m, n.

Русский

При заданном конечном κ и последовательностях a, y с условиями hay и ham можно построить объект VanishesTrivially из f, m, n.

LaTeX

$$$$ \\exists κ\\ [Fintype κ]\\ (a:ι→κ→R) (y:κ→N),\\; (\\forall i, n_i = \\sum_j a_{i j} y_j) \\land (\\forall j, \\sum_i a_{i j} m_i = 0) \\Rightarrow \\mathrm{TensorProduct.VanishesTrivially}\\ R\\ m\\ n.$$$$

Lean4

theorem of_fintype {κ} [Fintype κ] (a : ι → κ → R) (y : κ → N) (hay : ∀ i, n i = ∑ j, a i j • y j)
    (ham : ∀ j, ∑ i, a i j • m i = 0) : VanishesTrivially R m n :=
  have e := (Fintype.equivFin κ).symm
  ⟨Fintype.card κ, (a · ∘ e), y ∘ e, by simpa only [← e.sum_comp] using hay, by rwa [← e.forall_congr_right] at ham⟩

Похожие утверждения