Theorem smul_bot

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_bot View on Github →