## 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 $1\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):

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):

So I feel like we should have the full set

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: Aug 03 2023 at 10:10 UTC