Theorem Ideal.inertia_bot

Modification history

2026-09-26 10:13
Mathlib/RingTheory/Ideal/Pointwise.lean
feat(RingTheory/Ideal): the `⊥` and `⊤` cases of the pointwise action on ideals (#44070) …
Added Ideal.inertia_botView on Github →