Lemmas for Batteries.HashMap

Note that Lean core provides an alternative hash map implementation, Std.HashMap, which comes with more lemmas. See the module Std.Data.HashMap.Lemmas.

@[deprecated Std.HashMap.getElem?_empty (since := "2025-03-31")]

theorem Batteries.HashMap.empty_find? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅[a]? = none

Alias of Std.HashMap.getElem?_empty.