mul_nf — Mathlib

English

If two ONote elements are in normal form, then their product is in normal form.

Русский

Если два элемента ONote находятся в нормальной форме, то их произведение тоже в нормальной форме.

LaTeX

$$$\forall o_1,o_2\ [o_1\NF] [o_2\NF],\; (o_1 * o_2)\NF$$$

Lean4

instance mul_nf : ∀ (o₁ o₂) [NF o₁] [NF o₂], NF (o₁ * o₂)
  | 0, o, _, h₂ => by cases o <;> exact NF.zero
  | oadd _ _ _, _, ⟨⟨_, hb₁⟩⟩, ⟨⟨_, hb₂⟩⟩ => ⟨⟨_, oadd_mul_nfBelow hb₁ hb₂⟩⟩

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