ι_range_comap_reverse — Mathlib

English

The comap of the reverse map with respect to the range of ι_Q equals the range of ι_Q: (range (ι Q)).comap reverse = range (ι Q).

Русский

Сопряжение обратного отображения относительно диапазона ι_Q дает диапазон ι_Q: (range (ι Q)).comap reverse = range (ι Q).

LaTeX

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

Lean4

@[simp]
theorem ι_range_comap_reverse :
    (LinearMap.range (ι Q)).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = LinearMap.range (ι Q) := by
  rw [← submodule_map_reverse_eq_comap, ι_range_map_reverse]

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