Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_zero_class ℕ


Lars Ericson (Dec 14 2020 at 19:03):

There is a mul_zero_class by @Johan Commelin . is one, but I don't see it in mathlib:

import algebra.group_with_zero.defs
instance : mul_zero_class   := {
  mul := nat.has_mul.mul,
  zero := 0,
  zero_mul := nat.zero_mul,
  mul_zero := nat.mul_zero,
}

Maybe this could be included in data.nat.basic in the spirit of monoid:

import data.nat.basic
import algebra.group_with_zero.defs
#check nat.monoid -- nat.monoid : monoid ℕ
#check nat.mul_zero_class -- unknown identifier 'nat.mul_zero_class'

Adam Topaz (Dec 14 2020 at 19:05):

import data.nat.basic
#check (by apply_instance : mul_zero_class )

Adam Topaz (Dec 14 2020 at 19:05):

It comes from a monoid_with_zero instance for the naturals in this case.

Adam Topaz (Dec 14 2020 at 19:06):

Which, I guess, comes from the semiring structure on the naturals.

Adam Topaz (Dec 14 2020 at 19:08):

You can do a full trace like this, if you're interested;

import data.nat.basic
set_option trace.class_instances true
#check (by apply_instance : mul_zero_class )

Yury G. Kudryashov (Dec 15 2020 at 04:37):

I prefer set_option pp.all true to see the whole expression.


Last updated: Dec 20 2023 at 11:08 UTC