mul_single_apply_of_not_exists_mul

English

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

Русский

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

LaTeX

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

Lean4

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

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