IsAdjoinRoot.subsingleton

Stream: mathlib4

[Kenny Lau]

IsAdjoinRoot.subsingleton is completely redundant:

theorem IsAdjoinRoot.subsingleton {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : Polynomial R}
    [Algebra R S] (h : IsAdjoinRoot S f) [Subsingleton R] :
  Subsingleton S

because it's already implied by Algebra R S (and Subsingleton R) via RingHom.codomain_trivial:

import Mathlib

-- can't be an instance because `R` can't be inferred
lemma Subsingleton.of_algebra (R : Type*) [CommSemiring R] [Subsingleton R]
    (S : Type*) [Semiring S] [Algebra R S] :
    Subsingleton S :=
  (algebraMap R S).codomain_trivial

[Kenny Lau]

but actually the Subsingleton.of_algebra lemma is not in mathlib, and moreover once again it cannot be an instance, so it will be fundamentally less searchable

[Kenny Lau]

and the first redundant theorem is actually serving a purpose, because in a later part of the code, it is used:

        cases subsingleton_or_nontrivial R
        · subsingleton [h.subsingleton]

[Kenny Lau]

what's the best way to deal with this?

[Kenny Lau]

can we modify the nontriviality tactic to deal with this situation?

[Kenny Lau]

#29516

[Junyan Xu]

You can just use Module.subsingleton

[Kenny Lau]

well there's always more than one way to... uh... crack a nut