ι_range_map_reverse — Mathlib

English

The range of ι_Q is preserved under the reverse map: (range (ι Q)).map reverse = range (ι Q).

Русский

Диапазон ι_Q сохраняется под обратным отображением: (range (ι Q)).map reverse = range (ι Q).

LaTeX

$$$ (\mathrm{range}(\i_Q)).map (reverse) = \mathrm{range}(\i_Q) $$$

Lean4

@[simp]
theorem ι_range_map_reverse :
    (LinearMap.range (ι Q)).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = LinearMap.range (ι Q) :=
  by
  rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp, ← Submodule.map_comp]
  exact Submodule.map_id _

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