isTrivialRelation_comp — Mathlib

English

If the relation is trivial, then the sum over indices of f_i times x_i is zero.

Русский

Если отношение тривиально, то сумма по индексу i из f_i x_i равна нулю.

LaTeX

$$sum_smul_eq_zero_of_isTrivialRelation (h : IsTrivialRelation f x) : ∑ i, f i • x i = 0$$

Lean4

theorem _root_.Equiv.isTrivialRelation_comp {κ} [Fintype κ] (e : κ ≃ ι) :
    IsTrivialRelation (f ∘ e) (x ∘ e) ↔ IsTrivialRelation f x := by
  simp_rw [isTrivialRelation_iff_vanishesTrivially, e.vanishesTrivially_comp]

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