mul_zero_class ℕ

Stream: Is there code for X?

[Lars Ericson]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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