Theorems · Theorem · general algebraic systems

Finsupp.extendDomain.congr_simp

∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} {inst_1 : DecidablePred P} [inst_2 : DecidablePred P]
  (f f_1 : Subtype P →₀ M), f = f_1 → f.extendDomain = f_1.extendDomain

Defined in: Mathlib.Data.Finsupp.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero DecidablePred

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsuppstatement and proof · cited by 5,255
Finsupp.extendDomainstatement and proof · cited by 11

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.