instAddMonoidWithOne — Mathlib

English

If M is AddMonoidWithOne, then Germ_l M inherits AddMonoidWithOne structure, with natural embedding of zero and addition defined compatibly.

Русский

Если M — AddMonoidWithOne, то Germ_l M наследует AddMonoidWithOne, включая естественное вложение нуля и сложение.

LaTeX

$$$[AddMonoidWithOne\\ M] \\Rightarrow AddMonoidWithOne(\\mathrm{Germ}_l M).$$$

Lean4

instance instAddMonoidWithOne [AddMonoidWithOne M] : AddMonoidWithOne (Germ l M)
    where
  natCast_zero := congrArg ofFun <| by simp; rfl
  natCast_succ _ := congrArg ofFun <| by simp; rfl

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