Zulip Chat Archive

Stream: Is there code for X?

Topic: nontrivial matrices


view this post on Zulip Yakov Pechersky (Feb 18 2021 at 10:24):

Is there some pi instance that matches the following? Or is this just a missing hole in the lib?

import linear_algebra.matrix

instance {ι ι' R : Type*} [nontrivial R] [fintype ι] [fintype ι'] [inhabited ι] [inhabited ι'] :
  nontrivial (matrix ι ι' R) :=
exists.elim (exists_pair_ne R) $ λ x y, h⟩, λ _ _, x, λ _ _, y, by
  { contrapose! h, simpa using congr_fun (congr_fun h (default _)) (default _) }⟩⟩

view this post on Zulip Scott Morrison (Feb 18 2021 at 10:27):

It's in the library:

import linear_algebra.matrix

instance {ι ι' R : Type*} [nontrivial R] [fintype ι] [fintype ι'] [inhabited ι] [inhabited ι'] :
  nontrivial (matrix ι ι' R) :=
by { dsimp [matrix], apply_instance, }

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 10:30):

Thanks Scott! But it isn't automatically inferred without this declaration. Worth including?

view this post on Zulip Scott Morrison (Feb 18 2021 at 10:40):

I think so.

view this post on Zulip Eric Wieser (Feb 18 2021 at 10:57):

Similarly could add a subsingleton instance for [subsingleton R], and when we eventually have the typeclass, a unique instance for each of [empty ι] and [empty ι']

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 17:13):

We do already have:

lemma subsingleton_of_empty_left (hm : ¬ nonempty m) : subsingleton (matrix m n α) :=
λ M N, by { ext, contrapose! hm, use i }⟩

lemma subsingleton_of_empty_right (hn : ¬ nonempty n) : subsingleton (matrix m n α) :=
λ M N, by { ext, contrapose! hn, use j }⟩

Last updated: May 16 2021 at 05:21 UTC