instDistribMulActionOfRat — Mathlib

English

If α carries a distributive multiplication action by ℚ, then there is a corresponding DistribMulAction of ℚ≥0 on α obtained by restricting the ℚ-action.

Русский

Если α обладает распределимым умножением по ℚ, то существует соответствующее DistribMulAction по ℚ≥0 на α, получаемое ограничением ℚ-действия.

LaTeX

$$DistribMulAction ℚ α ⇒ DistribMulAction ℚ≥0 α$$

Lean4

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

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