TensorProduct.AlgebraTensorModule.curry_injective

theorem TensorProduct.AlgebraTensorModule.curry_injective : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P] [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P], Function.Injective TensorProduct.AlgebraTensorModule.curry

This theorem asserts that for all types `R`, `A`, `M`, `N`, `P`, equipped with certain algebraic structures (such as `CommSemiring`, `Semiring`, `Algebra`, `AddCommMonoid`, `Module`, and `IsScalarTower`), the `curry` function of the `AlgebraTensorModule` in the `TensorProduct` namespace is injective. In other words, if `curry f = curry g` then `f = g`. Here, `R`, `A` are rings, `M`, `N`, `P` are modules over the rings `R` and `A` with `M` and `P` forming a scalar tower over both `R` and `A` (meaning the action of `R` on `M` and `P` commutes with the action of `A`). Thus, the `curry` function, which maps linear maps from the tensor product of `M` and `N` to `P` into bilinear maps from `M` and `N` to `P`, is injective in this context.

More concisely: For types `R`, `A`, `M`, `N`, `P` being rings with certain algebraic structures and `M` and `P` forming a scalar tower over both, the `curry` function of the `AlgebraTensorModule` in Lean's `TensorProduct` namespace mapping bilinear maps from `M` and `N` to `P` to linear maps from the tensor product of `M` and `N` to `P` is injective.