Mathlib Map

Theorems · Theorem · general topology

Filter.pure_zero

∀ {α : Type u_2} [inst : Zero α], pure 0 = 0
Defined in
Mathlib.Order.Filter.Pointwise
Cited by
1 results in Mathlib
Foundations
Depth 13 from the axioms · uses propext
Assumes
Zero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Filter.pureZeroHom · cited by 2Filter.pureZeroHomFilter.add_eq_zero_iff · cited by 1Filter.add_eq_zero_iffFilter · cited by 8121FilterFilter.pure_zeroCITED BYCITES

Cites1

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

  • Filterstatement · cited by 8,121

Cited by2

Results whose statement or proof uses this declaration.