indToCoindAux_of_not_rel — Mathlib

English

If an element g1 is not related to g under right-rel relation of S, then indToCoindAux A g a g1 = 0.

Русский

Если элемент g1 не связан с g отношением справа относительно S, то indToCoindAux A g a g1 = 0.

LaTeX

$$$\neg ((QuotientGroup.rightRel S).r\; g1\; g) \Rightarrow indToCoindAux A g a g1 = 0$$$

Lean4

theorem indToCoindAux_of_not_rel (g g₁ : G) (a : A) (h : ¬(QuotientGroup.rightRel S).r g₁ g) :
    indToCoindAux A g a g₁ = 0 := by simp [indToCoindAux, dif_neg h]

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