Theorems · Theorem · general algebraic systems

Finsupp.eq_option_embedding_update_none_iff

∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {n : Option α →₀ M} {m : α →₀ M} {i : M},
  n = (Finsupp.embDomain Function.Embedding.some m).update none i ↔ n none = i ∧ n.some = m

Defined in

Mathlib.Data.Finsupp.Option

Cited by

1 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Zero