roption.dom vs multiplicity.finite

Stream: maths

[Johan Commelin]

We have docs#multiplicity.finite and

lemma finite_iff_dom [decidable_rel ((∣) : α → α → Prop)] {a b : α} :
  finite a b ↔ (multiplicity a b).dom := iff.rfl

what do people think of defining enat.finite instead (as abbreviation for roption.dom)?
Because data.nat.enat has many occurences of x.dom for some x : enat, and I think x.finite looks much better.

[Johan Commelin]

Maybe enat.finite shouldn't replace multiplicity.finite... both defs could coexist.