toQuotient_map_apply — Mathlib

English

For any x in the free A-module on G, the quotient map of the relation map applied to x is zero.

Русский

Для любого x из свободного модуля над G сумма образов через quotient-map равна нулю.

LaTeX

$$$\forall x \in (\text{relations.G} \to_A)\! A,\quad \text{relations.toQuotient}(\text{relations.map}(x)) = 0$$$

Lean4

@[simp]
theorem toQuotient_map_apply (x : relations.R →₀ A) : relations.toQuotient (relations.map x) = 0 :=
  DFunLike.congr_fun relations.toQuotient_map x

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