English
For any index i, the root span is contained in the invariant submodule associated to the reflection i; in particular, the root span is stabilized by the reflection.
Русский
Пусть для любого индекса i корневой охват лежит в инвариантной подсистеме, связанной с отражением i; то есть корневой охват сохраняется отражением.
LaTeX
$$$P{\cdot}rootSpan{R} \in Module.End.invtSubmodule(P.reflection i)$$$
Lean4
theorem rootSpan_mem_invtSubmodule_reflection (i : ι) : P.rootSpan R ∈ Module.End.invtSubmodule (P.reflection i) :=
by
rw [Module.End.mem_invtSubmodule, rootSpan]
intro x hx
induction hx using Submodule.span_induction with
| mem y hy =>
obtain ⟨j, rfl⟩ := hy
rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
apply Submodule.sub_mem
· exact Submodule.subset_span <| mem_range_self j
· exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
| zero => simp
| add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
| smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'
