mem_range_root_of_mem_range_reflection_of_mem_range_root

English

If r ∈ range P.reflection and α ∈ range P.root, then r · α ∈ range P.root.

Русский

Если r принадлежит range(P.reflection) и α принадлежит range(P.root), то r · α принадлежит range(P.root).

LaTeX

$$$ r \in \mathrm{range}(P.reflection) \ \land \alpha \in \mathrm{range}(P.root) \Rightarrow r \cdot \alpha \in \mathrm{range}(P.root) $$$

Lean4

theorem mem_range_root_of_mem_range_reflection_of_mem_range_root {r : M ≃ₗ[R] M} {α : M} (hr : r ∈ range P.reflection)
    (hα : α ∈ range P.root) : r • α ∈ range P.root :=
  by
  obtain ⟨i, rfl⟩ := hr
  obtain ⟨j, rfl⟩ := hα
  exact ⟨P.reflectionPerm i j, P.root_reflectionPerm i j⟩

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