English
`mulNat o n` is the ordinal notation for the product `o * n`; specifically: mulNat(0, _) = 0, mulNat(_, 0) = 0, and mulNat(oadd e n a, m+1) = oadd e (n * m.succPNat) a.
Русский
`mulNat o n` задаёт ординальное обозначение произведения `o * n`; конкретно: mulNat(0, _) = 0, mulNat(_, 0) = 0, и mulNat(oadd e n a, m+1) = oadd e (n * (m+1)) a.
LaTeX
$$$\text{mulNat}:\mathrm{ONote} \times \mathbb{N} \to \mathrm{ONote},\quad mulNat(0,\_)=0,\ mulNat(\_ ,0)=0,\ mulNat(oadd\ e\ n\ a,\ m+1)=oadd\ e\ (n\cdot m\!\;\text{succPNat})\ a.$$$
Lean4
/-- `mulNat o n` is the ordinal notation for `o * n`. -/
def mulNat : ONote → ℕ → ONote
| 0, _ => 0
| _, 0 => 0
| oadd e n a, m + 1 => oadd e (n * m.succPNat) a
