orbit_mk_eq_smul — Mathlib

English

In the quotient α / s, the orbit of x equals x.out • s.

Русский

В фактор-группе α / s орбита элемента x равна x.out • s.

LaTeX

$$$\mathrm{orbit}(x) = x^{\mathrm{out}} \cdot s$$$

Lean4

@[to_additive]
theorem orbit_mk_eq_smul (x : α) : MulAction.orbitRel.Quotient.orbit (x : α ⧸ s) = x • s :=
  by
  ext
  rw [orbitRel.Quotient.mem_orbit]
  simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _

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