Commit 2026-01-30 11:40 7d4bc899

View on Github →

chore: address linter warnings from lean PR 12225 (#34591) This PR fixes some linter warnings that came up on the adaptation branch of https://github.com/leanprover/lean4/pull/12225.

  • Removed some unused simp arguments
  • Removed some uses of change that didn't do anything

Estimated changes

modified theorem InfTopHom.coe_inf
modified theorem SupBotHom.coe_sup
modified theorem InfHom.coe_inf
modified theorem SupHom.coe_sup