Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,123 to 1,128 of 2,569 results.
FiniteAdeleRing.Aux.f_g_local_global
Mathematical statement
A diagram which obviously commutes, commutes.
Source project: Fermat's Last Theorem
Person-level attribution pending.
Finset.card_filter_prod_self_eq
Mathematical statement
The diagonal of s × s has the same cardinality as s.
Source project: ArkLib
Person-level attribution pending.
Finset.card_pick_subset
Mathematical statement
The cardinality of picked subset is min s.card n.
Source project: ArkLib
Person-level attribution pending.
Finset.card_prod_self_eq
Mathematical statement
The diagonal of s × s (intersection form) has the same cardinality as s.
Source project: ArkLib
Person-level attribution pending.
Finset.Shatters.toSetShatters
Mathematical statement
If a finite set family 𝒜 shatters a finite set s in the sense of Mathlib's Finset.Shatters, then the concept class of characteristic functions of sets in 𝒜 shatters ↑s in the sense of SetShatters. This bridges Mathlib's finset-based shattering to the predicate used by the PAC learning lower bounds.
Source project: Lean Computer Science Library
Person-level attribution pending.
Fischlin.almostComplete
Mathematical statement
Almost completeness of the Fischlin transform: if the underlying Σ-protocol is perfectly complete, then the signature scheme verifies with probability at least 1 - completenessError ρ b S t where t = FinEnum.card Chal is the challenge space size. Unlike the Fiat-Shamir transform (which is perfectly complete), the Fischlin transform has a non-zero comp...
Source project: VCVio
Person-level attribution pending.