nontrivial matrices

Stream: Is there code for X?

[Yakov Pechersky]

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 _) }⟩⟩

[Scott Morrison]

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

[Yakov Pechersky]

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

[Scott Morrison]

I think so.

[Eric Wieser]

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 ι']

[Yakov Pechersky]

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