instMonoidWithZero — Mathlib

English

WithZero α inherits a MonoidWithZero structure: powers and the zero element behave as in α, modulo the zero.

Русский

WithZero α наследует структуру MonoidWithZero: степени и ноль ведут себя как в α, с учётом нуля.

LaTeX

$$$\text{WithZero}(\alpha) \text{ has a MonoidWithZero structure}$$$

Lean4

instance instMonoidWithZero [Monoid α] : MonoidWithZero (WithZero α)
    where
  npow n a := a ^ n
  npow_zero
    | 0 => rfl
    | some _ => congr_arg some (pow_zero _)
  npow_succ
    | n, 0 => by simp only [mul_zero]; rfl
    | n, some _ => congr_arg some <| pow_succ _ _

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