map_apply_ι — Mathlib

English

The image of a single generator under the induced map is the corresponding generator: map f (ι_R m) = ι_R(f m).

Русский

Образ генератора под индуцированного отображения равен соответствующему генератору: map f (ι_R m) = ι_R(f m).

LaTeX

$$$ map_f(\\iota_R(m)) = \\iota_R(f(m)). $$$

Lean4

@[simp]
theorem map_apply_ι (f : M →ₗ[R] N) (m : M) : map f (ι R m) = ι R (f m) :=
  CliffordAlgebra.map_apply_ι _ m

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