Theorems · Theorem

Function.HasFiniteSupport.snd

∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {M' : Type u_3} [inst_1 : Zero M'] {f : α → M × M'},
  Function.HasFiniteSupport f → Function.HasFiniteSupport fun a => (f a).2

Defined in: Mathlib.Algebra.FiniteSupport.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero Zero

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.

Function.HasFiniteSupportstatement and proof · cited by 113
Function.HasFiniteSupport.compproof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.