mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot

English

If r ∈ range P.coreflection and α ∈ range P.coroot, then r · α ∈ range P.coroot.

Русский

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

LaTeX

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

Lean4

theorem mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot {r : N ≃ₗ[R] N} {α : N}
    (hr : r ∈ range P.coreflection) (hα : α ∈ range P.coroot) : r • α ∈ range P.coroot :=
  by
  obtain ⟨i, rfl⟩ := hr
  obtain ⟨j, rfl⟩ := hα
  exact ⟨P.reflectionPerm i j, P.coroot_reflectionPerm i j⟩

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