Theorem smul_top

Modification history

2026-09-26 10:13

Mathlib/Algebra/Order/Group/Action.lean

feat(RingTheory/Ideal): the `⊥` and `⊤` cases of the pointwise action on ideals (#44070) …

Added smul_top View on Github →