map_comp_apply — Mathlib

English

For f: T → R and g: R → S and any X in GL_n(T), applying map f to X and then map g to the result yields the same matrix as applying the composed map map(g ∘ f) to X.

Русский

Для f: T → R и g: R → S и любого X ∈ GL_n(T), применение map f к X, а затем применения map g к полученной матрице даёт ту же матрицу, что и применение map(g ∘ f) к X.

LaTeX

$$$(\\mathrm{map} \\ g) \\circ (\\mathrm{map} \\ f) (X) = \\mathrm{map} \\ g (\\mathrm{map} \\ f (X))$$$

Lean4

@[simp]
theorem map_comp_apply (f : T →+* R) (g : R →+* S) (x : GL n T) : (map g).comp (map f) x = map g (map f x) :=
  rfl

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