instMulActionOfRat — Mathlib

English

If α has a natural action by ℚ, then there is a corresponding action of ℚ≥0 on α by restriction of scalars.

Русский

Если у множества α есть действие по ℚ, то существует соответствующее действие ℚ≥0 на α как ограничение по подгруппе.

LaTeX

$$≤(MulAction)_{ℚ≥0} α := MulAction.compHom α (coeHom.toMonoidHom)$$

Lean4

/-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
  MulAction.compHom α coeHom.toMonoidHom

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