Documentation

PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support

source
theorem Function.support_id {α : Type u_1} [Zero α] :
support id = {0}ᶜ
Inspect dependencies

Function.support_id · compiled type and proof/definition references.

source
theorem Function.support_id' {α : Type u_2} [Zero α] :
(support fun (x : α) => x) = {0}ᶜ
Inspect dependencies

Function.support_id' · compiled type and proof/definition references.