coe_compAlternatingMap — Mathlib

English

The coercion of the composition equals the composition of the coercions.

Русский

Приведение к функции композиции совпадает с композицией приводящих отображений.

LaTeX

$$$ \operatorname{coe}\big( g \circ_{\mathrm{Alt}} f \big) = (\operatorname{coe} g) \circ \operatorname{AltMap.coe} f $$$

Lean4

@[simp]
theorem coe_compAlternatingMap (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) : ⇑(g.compAlternatingMap f) = g ∘ f :=
  rfl

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