Commit 2026-06-25 19:06 e7c715d3

View on Github →

chore: fix non-reducible diamond in StarRingEnd (#41047) The following fails before the PR, works after it

example : starRingEnd ℝ = RingHom.id ℝ := by
  with_reducible_and_instances rfl

Estimated changes

modified def starRingAut
modified def starRingEnd