Commit 2026-09-26 10:13 8accc048

feat(RingTheory/Ideal): the ⊥ and ⊤ cases of the pointwise action on ideals (#44070) Add the ⊥ and ⊤ versions of several results about pointwise actions, stabilizers and inertia subgroups, starting with smul_bot and smul_top: a group acting monotonically on an ordered type fixes ⊥ and ⊤. A few related results about the kernel of a ring homomorphism are added along the way, and some hypotheses and arguments are cleaned up. Prepared with Claude Code 🤖