English
For x,y in the nonzero elements of M, the relation of being in the same orbit under R^× equals the same relation in M itself: orbitRel Rˣ { v ∈ M | v ≠ 0 } x y ⇔ orbitRel Rˣ M x y.
Русский
Пусть x,y принадлежат ненулевым элементам M. Тогда Relation орбит равна в отношении орбит под действием R^× на подтипе ненулевых элементов и в полном M: orbitRel Rˣ { v ∈ M | v ≠ 0 } x y ⇔ orbitRel Rˣ M x y.
LaTeX
$$$ \\operatorname{orbitRel}(R^{\\times}, \\{ v \\in M \\mid v \\neq 0 \\})\\; x\\; y \\;\\iff\\; \\operatorname{orbitRel}(R^{\\times}, M)\\; x\\; y $$$
Lean4
theorem orbitRel_nonZero_iff (x y : { v : M // v ≠ 0 }) :
MulAction.orbitRel Rˣ { v // v ≠ 0 } x y ↔ MulAction.orbitRel Rˣ M x y :=
⟨by rintro ⟨a, rfl⟩; exact ⟨a, by simp⟩, by intro ⟨a, ha⟩; exact ⟨a, by ext; simpa⟩⟩
