Commit 2025-09-18 12:51 4b34167c

View on Github →

chore: Deprecate IsAdjoinRoot.subsingleton (#29516) This PR deprecates IsAdjoinRoot.subsingleton in favour of the new Algebra.subsingleton:

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
theorem Algebra.subsingleton (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A]
    [Subsingleton R] : Subsingleton A

Estimated changes

added theorem Algebra.subsingleton
modified theorem IsAdjoinRoot.subsingleton