Zulip Chat Archive

Stream: general

Topic: Is 0 not equal to 1?


Julian Külshammer (Nov 13 2021 at 15:39):

The question is about type classes I am not that familiar with: Do we have 101\neq 0 in a comm_cancel_monoid_with_zero which is also a normalized_gcd_monoid? The problem arose trying to prove a multiset version of lcm_eq_zero_iff. Here is my current attempt and the remaining sorry is to prove 1=0\to false:

import algebra.gcd_monoid.basic
import data.multiset.lattice

namespace multiset
variables {α : Type*} [comm_cancel_monoid_with_zero α] [normalized_gcd_monoid α]

theorem lcm_eq_zero_iff (s : multiset α) : s.lcm = 0  (0 : α)  s :=
begin
  split,
  { apply s.induction_on,
    { simp,
      sorry },
    { intros a s slcm h,
      rw mem_cons,
      rw [lcm_cons, lcm_eq_zero_iff] at h,
      cases h,
      { left,
        exact h.symm },
      { right,
        exact slcm h } } },
  { exact λ h, zero_dvd_iff.mp (dvd_lcm h) }
end
end multiset

Yaël Dillies (Nov 13 2021 at 15:45):

You need nontrivial α, then docs#one_ne_zero will do the job. It doesn't seem that normalized_gcd_monoid α implies nontrivial α:

import algebra.gcd_monoid.basic

example {α : Type*} [comm_cancel_monoid_with_zero α] [normalized_gcd_monoid α] : nontrivial α :=
by apply_instance -- fails

so you might just add [nontrivial α] to your lemma.

Julian Külshammer (Nov 13 2021 at 15:48):

Thanks, that does the job.

Eric Wieser (Nov 13 2021 at 15:53):

Your original statement is false:

import algebra.gcd_monoid.basic
import algebra.order.with_zero
import algebra.punit_instances

-- PR'd in #10312

instance : comm_cancel_monoid_with_zero punit :=
{ mul_left_cancel_of_ne_zero := λ _ _ _ _ _, subsingleton.elim _ _,
  mul_right_cancel_of_ne_zero := λ _ _ _ _ _, subsingleton.elim _ _,
  ..@comm_ring.to_comm_semiring _ punit.comm_ring}

instance : gcd_monoid punit :=
{ gcd := λ _ _, punit.star,
  lcm := λ _ _, punit.star,
  gcd_dvd_left := λ _ _, punit.star, subsingleton.elim _ _⟩,
  gcd_dvd_right := λ _ _, punit.star, subsingleton.elim _ _⟩,
  dvd_gcd := λ _ _ _ _ _, punit.star, subsingleton.elim _ _⟩,
  gcd_mul_lcm := λ _ _, 1, subsingleton.elim _ _⟩,
  lcm_zero_left := λ _, subsingleton.elim _ _,
  lcm_zero_right := λ _, subsingleton.elim _ _ }

instance : normalized_gcd_monoid punit :=
{ norm_unit := λ x, 1,
  norm_unit_zero := subsingleton.elim _ _,
  norm_unit_mul := λ _ _ _ _, subsingleton.elim _ _,
  norm_unit_coe_units := λ _, subsingleton.elim _ _,
  normalize_gcd := λ _ _, subsingleton.elim _ _,
  normalize_lcm := λ _ _, subsingleton.elim _ _,
  ..punit.gcd_monoid }

-- false
example : ¬∀ (α : Type*) [comm_cancel_monoid_with_zero α],
  by exactI  [normalized_gcd_monoid α], (0 : α)  1 :=
λ h, h unit (subsingleton.elim _ _)

Those instances should be in mathlib but seem not to be

Yaël Dillies (Nov 13 2021 at 15:54):

Surely you can generalize that to subsingleton α. But do we want all those "trivial" typeclasses?

Eric Wieser (Nov 13 2021 at 15:55):

We already have docs#punit.comm_ring

Eric Wieser (Nov 13 2021 at 15:55):

So I feel like we should have the full set

Yaël Dillies (Nov 13 2021 at 15:55):

Oh okay.

Eric Wieser (Nov 13 2021 at 15:55):

Deriving data from subsingleton α is a recipe for diamonds

Eric Wieser (Nov 13 2021 at 16:11):

PR'd as #10312, thankfully I didn't have to fix any import issues

Julian Külshammer (Nov 13 2021 at 16:22):

Thanks. Using this, in #10249 I was now able to define the exponent of a finite group and prove that it is the lcm of its orders.

Yury G. Kudryashov (Nov 13 2021 at 17:29):

One more reason to have instances on punit: this way we show that these typeclasses do not imply [nontrivial α].

Eric Wieser (Nov 13 2021 at 17:39):

I wonder if it would be valuable to have a linter that requires every typeclass either has a punit instance, implies nontrivial α, or is no-linted


Last updated: Dec 20 2023 at 11:08 UTC