English
Let R be a semiring and A a monoid with UniqueProds. Then the monoid algebra MonoidAlgebra(R, A) has the left-cancellation property with respect to multiplication by nonzero elements: if f ≠ 0 and f·g1 = f·g2, then g1 = g2.
Русский
Пусть R—полугруппа без нуля и A—моноид с уникальными произведениями. Тогда моноидальная алгебра MonoidAlgebra(R, A) обладает левым свойством отмены при умножении на ненулевой элемент: если f ≠ 0 и f·g1 = f·g2, то g1 = g2.
LaTeX
$$$\\forall f,g_1,g_2 \\in \\mathrm{MonoidAlgebra}(R,A),\\ f \\neq 0 \\Rightarrow (f g_1 = f g_2 \\Rightarrow g_1 = g_2).$$$
Lean4
instance [IsCancelAdd R] [IsLeftCancelMulZero R] [Mul A] [UniqueProds A] : IsLeftCancelMulZero (MonoidAlgebra R A) where
mul_left_cancel_of_ne_zero {f} hf {g₁ g₂}
eq := by
classical
induction hg : g₁.support ∪ g₂.support using Finset.eraseInduction generalizing g₁ g₂ with
| _ s ih =>
obtain h | h := s.eq_empty_or_nonempty <;> subst s
· simp_rw [Finset.union_eq_empty, support_eq_empty] at h; exact h.1.trans h.2.symm
have ⟨af, haf, ag, hag, uniq⟩ := UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.2 hf) h
have h := mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
dsimp only at eq
rw [eq, mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
have := mul_left_cancel₀ (mem_support_iff.mp haf) h
rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
simp_rw [mul_add, add_right_cancel_iff] at eq
rw [ih ag hag eq]
simp_rw [support_erase, Finset.erase_union_distrib]
