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 44 research declarations. Search 10,000 more complete Mathlib declarations.
44 results
Clear filtersList.mapM'_some_iff_forall₂
Plain-language statement
Copy of mapM'_ok_iff_forall₂ but for option instead of exception
Source project: Cedar Specification
Person-level attribution pending.
SM.SMNoGrav.One.accGrav_Q_zero
Plain-language statement
For a set of 1-family SM charges satisfying all ACCs except the gravitational, if the Q charge is zero then the charges satisfy the gravitational ACCs.
Source project: Physlib
Person-level attribution pending.