isSMulRegular_iff — Mathlib

English

If each R i carries an action by α and each R i is nonempty, then IsSMulRegular on the product ∀ i, R i with respect to r ∈ α is equivalent to IsSMulRegular on each factor.

Русский

Пусть каждый R_i имеет действие α; если для каждого i выполнено, что R_i непусто, то IsSMulRegular на произведении ∀ i, R_i в отношении r эквивалентно IsSMulRegular на каждом факторе.

LaTeX

$$$IsSMulRegular(\forall i, R_i)\ r \iff \forall i, IsSMulRegular(R_i)\ r$$$

Lean4

@[simp]
theorem isSMulRegular_iff [∀ i, SMul α (R i)] {r : α} [∀ i, Nonempty (R i)] :
    IsSMulRegular (∀ i, R i) r ↔ ∀ i, IsSMulRegular (R i) r :=
  Pi.map_injective

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