Theorem: Subideal.bot_def (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
⊢ ⟨⊥, ⋯⟩ = ⊥
Tactic:
rw [mk_bot]
State after:
no goals