Commit 2025-10-01 07:52 7438734e

View on Github →

chore: fix type confusion in LatticeHom.withTop/withBot/withTopWithBot (#30100) Based on #27918.

Estimated changes

modified theorem LatticeHom.coe_withBot