orbitRel_of_subMul — Mathlib

English

For any p and m ∈ p, the stabilizer of m in R equals the stabilizer of its underlying element in M.

Русский

Для p и m ∈ p стабилизатор m в R равен стабилизатору его базового элемента в M.

LaTeX

$$$ MulAction.stabilizer\\ R\\ m = MulAction.stabilizer\\ R\\ (m : M) $$$

Lean4

@[to_additive]
theorem orbitRel_of_subMul (p : SubMulAction R M) :
    MulAction.orbitRel R p = (MulAction.orbitRel R M).comap Subtype.val :=
  by
  refine Setoid.ext_iff.2 (fun x y ↦ ?_)
  rw [Setoid.comap_rel]
  exact mem_orbit_subMul_iff

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