C_mul_monomial — Mathlib

English

Equality of monomials with the same coefficient implies equality of exponents when the coefficient is nonzero.

Русский

Равенство мономов с одинаковым коэффициентом при ненулевом коэффициенте означает равенство показателей степени.

LaTeX

$$$ hr \neq 0 \rightarrow (monomial\, s\, r = monomial\, t\, r \leftrightarrow s = t)$$$

Lean4

theorem C_mul_monomial : C a * monomial s a' = monomial s (a * a') := by
  -- Porting note: this `change` feels like defeq abuse, but I can't find the appropriate lemmas

  change AddMonoidAlgebra.single _ _ * AddMonoidAlgebra.single _ _ = AddMonoidAlgebra.single _ _
  simp [single_mul_single]

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