Commit 2025-08-09 00:27 faf61920

View on Github →

chore(RingTheory/IsAdjoinRoot): refactor IsAdjoinRoot (#27367)

  • Change definition of IsAdjoinRoot to use bundled AlgHom
  • Remove duplicated API for AdjoinRoot.isAdjoinRootMonic
  • Remove bad simp lemma isAdjoinRoot_map_eq_mk
  • Make map_repr simp
  • Rename some lemmas to be more descriptive The data of IsAdjoinRoot is determined by IsAdjoinRoot.root. The simp normal form was previously unclear; now it runs through simplifying IsAdjoinRoot.root rather than IsAdjoinRoot.map.

Estimated changes

added theorem AdjoinRoot.coe_mkₐ
added def AdjoinRoot.mkₐ
modified theorem IsAdjoinRoot.aequiv_symm
deleted theorem IsAdjoinRoot.aeval_eq
deleted theorem IsAdjoinRoot.aeval_root
modified theorem IsAdjoinRoot.lift_self