mk_zero_smul — Mathlib

English

Given a ∈ A 0 and b ∈ A i, the product mk i (a • b) equals mk 0 a times mk i b.

Русский

Пусть a ∈ A 0 и b ∈ A i. Тогда произведение mk i (a • b) равно mk 0 a умножить на mk i b.

LaTeX

$$$\\mathrm{mk}\\ i\$a \\cdot b\$ = \\mathrm{mk}\\ 0\\ a \\cdot \\mathrm{mk}\\ i\\ b$$$

Lean4

@[simp]
theorem mk_zero_smul {i} (a : A 0) (b : A i) : mk _ (a • b) = mk _ a * mk _ b :=
  Sigma.ext (zero_add _).symm <| eqRec_heq _ _

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