[Merged by Bors] - feat(LinearAlgebra/PiTensorProduct): make reindex dependently typed
#9445
Conversation
jjaassoonn
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| #align pi_tensor_product.reindex PiTensorProduct.reindex | ||
|
|
||
| end | ||
|
|
||
| @[simp] | ||
| theorem reindex_tprod (e : ι ≃ ι₂) (f : ι → M) : | ||
| reindex R M e (tprod R f) = tprod R fun i ↦ f (e.symm i) := by | ||
| theorem reindex_tprod (e : ι ≃ ι₂) (f : ∀ i, s i) : |
There was a problem hiding this comment.
Can you use a different notation for the dependent function type? I really think ∀ should be reserved for propositions.
There was a problem hiding this comment.
This is changed as well as other inappropriate \forall in this file. Not sure if I missed anything
| congr | ||
| ext | ||
| rw [e.symm_apply_apply]) | ||
| variable (s) in |
There was a problem hiding this comment.
What do you think about making s implicit? I understand that then one has to write (s := ...) to use the dependent version, but I think people will use much more the non dependent one, and maybe Lean is able to guess it in that case (of course if (s := ...) is needed also in the nondependent case this comment is pointless).
There was a problem hiding this comment.
Lean can find the constant (s := fun _ => M) if we give it enough hint.
(reindex R e : (⨂[R] _, M) ≃ₗ[R] ⨂[R] _, M)There was a problem hiding this comment.
Since implicit s need type hinting in non-dependent cases as well, I have decided to make s explicit, so non-dependent case will be reindex R (fun _ => M) e
|
Thanks! bors d+ |
|
✌️ jjaassoonn can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
bors r+ |
…#9445) used to be `(⨂[R] _ : ι, M) ≃ₗ[R] ⨂[R] _ : ι₂, M`, now `M` can vary according to the indexing set. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
reindex dependently typedreindex dependently typed
used to be
(⨂[R] _ : ι, M) ≃ₗ[R] ⨂[R] _ : ι₂, M, nowMcan vary according to the indexing set.