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 4 research declarations. Search 10,000 more complete Mathlib declarations.
4 results
Clear filtersTensorSpecies.Tensor.IsReindexing.contr_two_rotate
Plain-language statement
Contracting the i-th index of a tensor with the first index of an appended metric tensor is, up to a cycle permutation, a reindexing to the color list where the i-th index is replaced by its dual.
Source project: Physlib
Person-level attribution pending.
TensorSpecies.Tensor.IsReindexing.succAbove_of_eq_zero
Plain-language statement
Given a reindexing of c by c1 via σ for which the index i is sent to 0, removing the i-th entry of c1 and the first entry of c yields a reindexing of c ∘ Fin.succ by c1 ∘ i.succAbove via the map sending j to the predecessor of σ (i.succAbove j).
Source project: Physlib
Person-level attribution pending.
TensorSpecies.Tensor.IsReindexing.succAbove_of_neq_zero
Plain-language statement
Given a reindexing of c by c1 via σ for which the index i is not sent to 0, removing the i-th entry of c1 and the (σ i)-th entry of c yields a reindexing of c ∘ (σ i).succAbove by c1 ∘ i.succAbove via the map (σ i).pred.predAbove ∘ σ ∘ i.succAbove.
Source project: Physlib
Person-level attribution pending.
TensorSpecies.Tensor.IsReindexing.succSuccAbove_comm
Plain-language statement
Removing two pairs of entries from c in either order gives the same colour list: removing the i1-th and j1-th entries and then the (shifted) i2-th and j2-th entries matches removing the i2-th and j2-th entries first and then the (shifted) i1-th and j1-th entries, via the identity permutation. This is used for the commutation of two *cont...
Source project: Physlib
Person-level attribution pending.