isSMulRegular_of_group — Mathlib

English

An element g of a group acting on a Type is regular.

Русский

Элемент группы G, действующий на множество, является регулярен.

LaTeX

$$$IsSMulRegular M g$ for any g ∈ G with group structure$$

Lean4

/-- An element of a group acting on a Type is regular. This relies on the availability
of the inverse given by groups, since there is no `LeftCancelSMul` typeclass. -/
theorem isSMulRegular_of_group [MulAction G R] (g : G) : IsSMulRegular R g :=
  by
  intro x y h
  convert congr_arg (g⁻¹ • ·) h using 1 <;> simp [← smul_assoc]

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