single_mul_apply_of_not_exists_mul

English

If there is no d with m' = m·d, then (single m r * x) at m' equals 0.

Русский

Если не существует d с m' = m·d, то (single m r * x) в m' равно 0.

LaTeX

$$$\text{If } \nexists d,\; m' = m d\text{, then } (\operatorname{single}(m,r) * x)(m') = 0$$$

Lean4

@[to_additive (attr := simp) (dont_translate := R) single_mul_apply_of_not_exists_add]
theorem single_mul_apply_of_not_exists_mul (r : R) (x : MonoidAlgebra R M) (h : ¬∃ d, m' = m * d) :
    (single m r * x) m' = 0 := by classical simp_all [mul_apply, eq_comm]

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