instAddGroupWithOne — Mathlib

English

If R is nontrivial and l is nonempty (NeBot), then Germ l R is nontrivial.

Русский

Если R ненулевой и l не пуст, то Germ l R ненулевой.

LaTeX

$$$ \\text{Nontrivial}( \\mathrm{Germ}(l,R) ). $$$

Lean4

instance instAddGroupWithOne [AddGroupWithOne G] : AddGroupWithOne (Germ l G)
    where
  __ := instAddMonoidWithOne
  __ := instAddGroup
  intCast_ofNat _ := congrArg ofFun <| by simp
  intCast_negSucc _ := congrArg ofFun <| by simp [Function.comp_def]; rfl

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