Revision #1537 → #2639 · back to history
modifiedComponent of a tensorb8fca719f9bd
| Field | From #1537 | To #2639 |
|---|
| mathlib.decl | Basis.repr | Module.Basis.repr |
| provenance | ai | ai-moderated |
modifiedTensor contractiond400a84608a3
| Field | From #1537 | To #2639 |
|---|
| mathlib.decl | TensorProduct.contractLeft | contractLeft |
| provenance | ai | ai-moderated |
modifiedTensor equality componentwiseb01e52f93333
| Field | From #1537 | To #2639 |
|---|
| mathlib.decl | Basis.ext_elem_iff | Module.Basis.ext_elem_iff |
| provenance | ai | ai-moderated |
modifiedMetric tensor and length of curves26c6c12744ae
| Field | From #1537 | To #2639 |
|---|
| mathlib.decl | RiemannianMetric | Bundle.RiemannianMetric |
| provenance | ai | ai-moderated |