therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.32.0

Tensor Product localcomponent apply

IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply

Plain-language statement

If Ļ† : š”ø_K^f āŠ— V ā†’ š”ø_K^f āŠ— V is š”ø_K^f-linear and Ļ†ā‚š is its local component at a place p then for all x : š”ø_K^f āŠ— V we have (evalā‚š āŠ— id_V) (Ļ† x) = Ļ†ā‚š ((evalā‚š āŠ— id_V) x), or, more colloquiually, (Ļ† x)ā‚š = Ļ†ā‚š (xā‚š).

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record