fixedBy_eq_univ_iff_eq_one — Mathlib

English

If g and h commute, then g fixes (h^j) • x if and only if g fixes x; equivalently, the moved-by set is fixed by h.

Русский

Если g и h коммутируют, то g фиксирует (h^j) • x тогда и только тогда, когда g фиксирует x; иначе говоря, множество перемещаемого фиксируется h.

LaTeX

$$$ h^{j} \cdot (fixedBy α g) = fixedBy α g $$$

Lean4

/-- If the multiplicative action of `M` on `α` is faithful,
then `fixedBy α m = Set.univ` implies that `m = 1`. -/
@[to_additive /-- If the additive action of `M` on `α` is faithful,
    then `fixedBy α m = Set.univ` implies that `m = 1`. -/
    ]
theorem fixedBy_eq_univ_iff_eq_one {m : M} : fixedBy α m = Set.univ ↔ m = 1 :=
  by
  rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall]
  simp_rw [funext_iff, one_smul, mem_fixedBy]

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