Commit 2026-10-01 17:54 87fc9444

View on Github →

chore: fix an implicit reducible diamond in shrinked normed spaces (#44130) The following fails before the PR, works after it:

example [SeminormedAddCommGroup α] [NormedSpace 𝕜 α] : 
    (Shrink.instNormedSpace.toMulAction : MulAction 𝕜 (Shrink.{v} α)) = 
    Shrink.instMulAction := by
  with_implicit rfl

Estimated changes