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