mul_iff_right — Mathlib

English

For any a, IsSMulRegular M a implies IsSMulRegular M (a*b) is equivalent to IsSMulRegular M b.

Русский

Для любого a: IsSMulRegular M a ⇒ IsSMulRegular M (a*b) эквивалентно IsSMulRegular M b.

LaTeX

$$[simp] IsSMulRegular M a → (IsSMulRegular M (instHMul.hMul a b) ↔ IsSMulRegular M b)$$

Lean4

@[simp]
theorem mul_iff_right [Mul R] [IsScalarTower R R M] (ha : IsSMulRegular M a) :
    IsSMulRegular M (a * b) ↔ IsSMulRegular M b :=
  ⟨of_mul, ha.mul⟩

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