map_comp — Mathlib

English

Naturality of the quotient–tensor equivalence with respect to f.

Русский

Естественность эквивалентности между квотированием и тензором по отношению к f.

LaTeX

$$$$ EquivQuotTensor(r,M') \circ map\_r f = f\_tensor \, EquivQuotTensor(r,M). $$$$

Lean4

@[simp]
theorem map_comp (g : M' →ₗ[R] M'') (f : M →ₗ[R] M') : map r (g ∘ₗ f) = map r g ∘ₗ map r f :=
  DFunLike.ext _ _ <| (mkQ_surjective _).forall.mpr fun _ => rfl

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