curry_injective — Mathlib

English

Compatibility of curry with restrictScalars: (restrictScalars R) (curry f) equals curry of (restrictScalars R f).

Русский

Совместимость карри с ограничением скаляров: (restrictScalars R) (curry f) равняется curry (restrictScalars R f).

LaTeX

$$restrictScalars R (TensorProduct.AlgebraTensorModule.curry f) = TensorProduct.curry (f.restrictScalars R)$$

Lean4

/-- Just as `TensorProduct.ext` is marked `ext` instead of `TensorProduct.ext'`, this is
a better `ext` lemma than `TensorProduct.AlgebraTensorModule.ext` below.

See note [partially-applied ext lemmas]. -/
@[ext high]
nonrec theorem curry_injective : Function.Injective (curry : (M ⊗ N →ₗ[A] P) → M →ₗ[A] N →ₗ[R] P) := fun _ _ h =>
  LinearMap.restrictScalars_injective R <| curry_injective <| (congr_arg (LinearMap.restrictScalars R) h :)

Похожие утверждения