# mathlib3documentation

linear_algebra.multilinear.basic

# Multilinear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define multilinear maps as maps from `Π(i : ι), M₁ i` to `M₂` which are linear in each coordinate. Here, `M₁ i` and `M₂` are modules over a ring `R`, and `ι` is an arbitrary type (although some statements will require it to be a fintype). This space, denoted by `multilinear_map R M₁ M₂`, inherits a module structure by pointwise addition and multiplication.

## Main definitions #

• `multilinear_map R M₁ M₂` is the space of multilinear maps from `Π(i : ι), M₁ i` to `M₂`.
• `f.map_smul` is the multiplicativity of the multilinear map `f` along each coordinate.
• `f.map_add` is the additivity of the multilinear map `f` along each coordinate.
• `f.map_smul_univ` expresses the multiplicativity of `f` over all coordinates at the same time, writing `f (λi, c i • m i)` as `(∏ i, c i) • f m`.
• `f.map_add_univ` expresses the additivity of `f` over all coordinates at the same time, writing `f (m + m')` as the sum over all subsets `s` of `ι` of `f (s.piecewise m m')`.
• `f.map_sum` expresses `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` as the sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all possible functions.

We also register isomorphisms corresponding to currying or uncurrying variables, transforming a multilinear function `f` on `n+1` variables into a linear function taking values in multilinear functions in `n` variables, and into a multilinear function in `n` variables taking values in linear functions. These operations are called `f.curry_left` and `f.curry_right` respectively (with inverses `f.uncurry_left` and `f.uncurry_right`). These operations induce linear equivalences between spaces of multilinear functions in `n+1` variables and spaces of linear functions into multilinear functions in `n` variables (resp. multilinear functions in `n` variables taking values in linear functions), called respectively `multilinear_curry_left_equiv` and `multilinear_curry_right_equiv`.

## Implementation notes #

Expressing that a map is linear along the `i`-th coordinate when all other coordinates are fixed can be done in two (equivalent) different ways:

• fixing a vector `m : Π(j : ι - i), M₁ j.val`, and then choosing separately the `i`-th coordinate
• fixing a vector `m : Πj, M₁ j`, and then modifying its `i`-th coordinate

The second way is more artificial as the value of `m` at `i` is not relevant, but it has the advantage of avoiding subtype inclusion issues. This is the definition we use, based on `function.update` that allows to change the value of `m` at `i`.

Note that the use of `function.update` requires a `decidable_eq ι` term to appear somewhere in the statement of `multilinear_map.map_add'` and `multilinear_map.map_smul'`. Three possible choices are:

1. Requiring `decidable_eq ι` as an argument to `multilinear_map` (as we did originally).
2. Using `classical.dec_eq ι` in the statement of `map_add'` and `map_smul'`.
3. Quantifying over all possible `decidable_eq ι` instances in the statement of `map_add'` and `map_smul'`.

Option 1 works fine, but puts unecessary constraints on the user (the zero map certainly does not need decidability). Option 2 looks great at first, but in the common case when `ι = fin n` it introduces non-defeq decidability instance diamonds within the context of proving `map_add'` and `map_smul'`, of the form `fin.decidable_eq n = classical.dec_eq (fin n)`. Option 3 of course does something similar, but of the form `fin.decidable_eq n = _inst`, which is much easier to clean up since `_inst` is a free variable and so the equality can just be substituted.

structure multilinear_map (R : Type u) {ι : Type u'} (M₁ : ι Type v) (M₂ : Type w) [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
Type (max u' v w)
• to_fun : (Π (i : ι), M₁ i) M₂
• map_add' : [_inst_1_1 : (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i), self.to_fun i (x + y)) = self.to_fun i x) + self.to_fun i y)
• map_smul' : [_inst_1_1 : (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), self.to_fun i (c x)) = c self.to_fun i x)

Multilinear maps over the ring `R`, from `Πi, M₁ i` to `M₂` where `M₁ i` and `M₂` are modules over `R`.

Instances for `multilinear_map`
@[protected, instance]
def multilinear_map.has_coe_to_fun {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
has_coe_to_fun M₁ M₂) (λ (f : M₁ M₂), (Π (i : ι), M₁ i) M₂)
Equations
@[simp]
theorem multilinear_map.to_fun_eq_coe {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) :
@[simp]
theorem multilinear_map.coe_mk {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : (Π (i : ι), M₁ i) M₂) (h₁ : [_inst_1 : (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i), f i (x + y)) = f i x) + f i y)) (h₂ : [_inst_1_1 : (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), f i (c x)) = c f i x)) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
theorem multilinear_map.congr_fun {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {f g : M₁ M₂} (h : f = g) (x : Π (i : ι), M₁ i) :
f x = g x
theorem multilinear_map.congr_arg {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) {x y : Π (i : ι), M₁ i} (h : x = y) :
f x = f y
theorem multilinear_map.coe_injective {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
@[simp, norm_cast]
theorem multilinear_map.coe_inj {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {f g : M₁ M₂} :
f = g f = g
@[ext]
theorem multilinear_map.ext {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {f f' : M₁ M₂} (H : (x : Π (i : ι), M₁ i), f x = f' x) :
f = f'
theorem multilinear_map.ext_iff {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {f g : M₁ M₂} :
f = g (x : Π (i : ι), M₁ i), f x = g x
@[simp]
theorem multilinear_map.mk_coe {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) (h₁ : [_inst_1_1 : (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i), f i (x + y)) = f i x) + f i y)) (h₂ : [_inst_1_1 : (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), f i (c x)) = c f i x)) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
@[protected, simp]
theorem multilinear_map.map_add {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i) :
f i (x + y)) = f i x) + f i y)
@[protected, simp]
theorem multilinear_map.map_smul {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i) :
f i (c x)) = c f i x)
theorem multilinear_map.map_coord_zero {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) {m : Π (i : ι), M₁ i} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem multilinear_map.map_update_zero {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) :
f i 0) = 0
@[simp]
theorem multilinear_map.map_zero {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [nonempty ι] :
f 0 = 0
@[protected, instance]
def multilinear_map.has_add {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
Equations
@[simp]
theorem multilinear_map.add_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f f' : M₁ M₂) (m : Π (i : ι), M₁ i) :
(f + f') m = f m + f' m
@[protected, instance]
def multilinear_map.has_zero {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
has_zero M₁ M₂)
Equations
@[protected, instance]
def multilinear_map.inhabited {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
inhabited M₁ M₂)
Equations
@[simp]
theorem multilinear_map.zero_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (m : Π (i : ι), M₁ i) :
0 m = 0
@[protected, instance]
def multilinear_map.has_smul {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ R' M₂] :
has_smul R' M₁ M₂)
Equations
@[simp]
theorem multilinear_map.smul_apply {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ R' M₂] (f : M₁ M₂) (c : R') (m : Π (i : ι), M₁ i) :
(c f) m = c f m
theorem multilinear_map.coe_smul {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ R' M₂] (c : R') (f : M₁ M₂) :
(c f) = c f
@[protected, instance]
def multilinear_map.add_comm_monoid {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] :
Equations
@[simp]
theorem multilinear_map.sum_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {α : Type u_1} (f : α M₁ M₂) (m : Π (i : ι), M₁ i) {s : finset α} :
(s.sum (λ (a : α), f a)) m = s.sum (λ (a : α), (f a) m)
def multilinear_map.to_linear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) :
M₁ i →ₗ[R] M₂

If `f` is a multilinear map, then `f.to_linear_map m i` is the linear map obtained by fixing all coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate.

Equations
@[simp]
theorem multilinear_map.to_linear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x : M₁ i) :
(f.to_linear_map m i) x = f i x)
def multilinear_map.prod {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] (f : M₁ M₂) (g : M₁ M₃) :
M₁ (M₂ × M₃)

The cartesian product of two multilinear maps, as a multilinear map.

Equations
@[simp]
theorem multilinear_map.prod_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] (f : M₁ M₂) (g : M₁ M₃) (m : Π (i : ι), M₁ i) :
(f.prod g) m = (f m, g m)
@[simp]
theorem multilinear_map.pi_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), (M' i)] (f : Π (i : ι'), M₁ (M' i)) (m : Π (i : ι), M₁ i) (i : ι') :
m i = (f i) m
def multilinear_map.pi {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), (M₁ i)] {ι' : Type u_1} {M' : ι' Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), (M' i)] (f : Π (i : ι'), M₁ (M' i)) :
M₁ (Π (i : ι'), M' i)

Combine a family of multilinear maps with the same domain and codomains `M' i` into a multilinear map taking values in the space of functions `Π i, M' i`.

Equations
@[simp]
theorem multilinear_map.of_subsingleton_apply (R : Type u) {ι : Type u'} (M₂ : Type v₂) [semiring R] [add_comm_monoid M₂] [ M₂] [subsingleton ι] (i' : ι) (f : Π (x : ι), (λ (i : ι), M₂) x) :
i') f = f
def multilinear_map.of_subsingleton (R : Type u) {ι : Type u'} (M₂ : Type v₂) [semiring R] [add_comm_monoid M₂] [ M₂] [subsingleton ι] (i' : ι) :
(λ (_x : ι), M₂) M₂

The evaluation map from `ι → M₂` to `M₂` is multilinear at a given `i` when `ι` is subsingleton.

Equations
def multilinear_map.const_of_is_empty (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [is_empty ι] (m : M₂) :
M₁ M₂

The constant map is multilinear when `ι` is empty.

Equations
@[simp]
theorem multilinear_map.const_of_is_empty_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [is_empty ι] (m : M₂) :
= function.const (Π (i : ι), M₁ i) m
def multilinear_map.restr {R : Type u} {M₂ : Type v₂} {M' : Type v'} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M'] [ M₂] [ M'] {k n : } (f : (λ (i : fin n), M') M₂) (s : finset (fin n)) (hk : s.card = k) (z : M') :
(λ (i : fin k), M') M₂

Given a multilinear map `f` on `n` variables (parameterized by `fin n`) and a subset `s` of `k` of these variables, one gets a new multilinear map on `fin k` by varying these variables, and fixing the other ones equal to a given value `z`. It is denoted by `f.restr s hk z`, where `hk` is a proof that the cardinality of `s` is `k`. The implicit identification between `fin k` and `s` that we use is the canonical (increasing) bijection.

Equations
theorem multilinear_map.cons_add {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) (m : Π (i : fin n), M i.succ) (x y : M 0) :
f (fin.cons (x + y) m) = f (fin.cons x m) + f (fin.cons y m)

In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the additivity of a multilinear map along the first variable.

theorem multilinear_map.cons_smul {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) (m : Π (i : fin n), M i.succ) (c : R) (x : M 0) :
f (fin.cons (c x) m) = c f (fin.cons x m)

In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the multiplicativity of a multilinear map along the first variable.

theorem multilinear_map.snoc_add {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) (m : Π (i : fin n), M ) (x y : M (fin.last n)) :
f (fin.snoc m (x + y)) = f (fin.snoc m x) + f (fin.snoc m y)

In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `snoc`, one can express directly the additivity of a multilinear map along the first variable.

theorem multilinear_map.snoc_smul {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) (m : Π (i : fin n), M ) (c : R) (x : M (fin.last n)) :
f (fin.snoc m (c x)) = c f (fin.snoc m x)

In the specific case of multilinear maps on spaces indexed by `fin (n+1)`, where one can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the multiplicativity of a multilinear map along the first variable.

def multilinear_map.comp_linear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (g : M₁' M₂) (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) :
M₁ M₂

If `g` is a multilinear map and `f` is a collection of linear maps, then `g (f₁ m₁, ..., fₙ mₙ)` is again a multilinear map, that we call `g.comp_linear_map f`.

Equations
@[simp]
theorem multilinear_map.comp_linear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (g : M₁' M₂) (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) (m : Π (i : ι), M₁ i) :
(g.comp_linear_map f) m = g (λ (i : ι), (f i) (m i))
theorem multilinear_map.comp_linear_map_assoc {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] {M₁'' : ι Type u_2} [Π (i : ι), add_comm_monoid (M₁'' i)] [Π (i : ι), (M₁'' i)] (g : M₁'' M₂) (f₁ : Π (i : ι), M₁' i →ₗ[R] M₁'' i) (f₂ : Π (i : ι), M₁ i →ₗ[R] M₁' i) :
(g.comp_linear_map f₁).comp_linear_map f₂ = g.comp_linear_map (λ (i : ι), (f₁ i).comp (f₂ i))

Composing a multilinear map twice with a linear map in each argument is the same as composing with their composition.

@[simp]
theorem multilinear_map.zero_comp_linear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) :
= 0

Composing the zero multilinear map with a linear map in each argument.

@[simp]
theorem multilinear_map.comp_linear_map_id {R : Type u} {ι : Type u'} {M₂ : Type v₂} [semiring R] [add_comm_monoid M₂] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (g : M₁' M₂) :
g.comp_linear_map (λ (i : ι), linear_map.id) = g

Composing a multilinear map with the identity linear map in each argument.

theorem multilinear_map.comp_linear_map_injective {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) (hf : (i : ι), function.surjective (f i)) :
function.injective (λ (g : M₁' M₂), g.comp_linear_map f)

Composing with a family of surjective linear maps is injective.

theorem multilinear_map.comp_linear_map_inj {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) (hf : (i : ι), function.surjective (f i)) (g₁ g₂ : M₁' M₂) :
g₁.comp_linear_map f = g₂.comp_linear_map f g₁ = g₂
@[simp]
theorem multilinear_map.comp_linear_equiv_eq_zero_iff {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), (M₁' i)] (g : M₁' M₂) (f : Π (i : ι), M₁ i ≃ₗ[R] M₁' i) :
g.comp_linear_map (λ (i : ι), (f i)) = 0 g = 0

Composing a multilinear map with a linear equiv on each argument gives the zero map if and only if the multilinear map is the zero map.

theorem multilinear_map.map_piecewise_add {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m m' : Π (i : ι), M₁ i) (t : finset ι) :
f (t.piecewise (m + m') m') = t.powerset.sum (λ (s : finset ι), f (s.piecewise m m'))

If one adds to a vector `m'` another vector `m`, but only for coordinates in a finset `t`, then the image under a multilinear map `f` is the sum of `f (s.piecewise m m')` along all subsets `s` of `t`. This is mainly an auxiliary statement to prove the result when `t = univ`, given in `map_add_univ`, although it can be useful in its own right as it does not require the index set `ι` to be finite.

theorem multilinear_map.map_add_univ {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] [fintype ι] (m m' : Π (i : ι), M₁ i) :
f (m + m') = finset.univ.sum (λ (s : finset ι), f (s.piecewise m m'))

Additivity of a multilinear map along all coordinates at the same time, writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`.

theorem multilinear_map.map_sum_finset_aux {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) {α : ι Type u_1} (g : Π (i : ι), α i M₁ i) (A : Π (i : ι), finset (α i)) [decidable_eq ι] [fintype ι] {n : } (h : finset.univ.sum (λ (i : ι), (A i).card) = n) :
f (λ (i : ι), (A i).sum (λ (j : α i), g i j)) = .sum (λ (r : Π (a : ι), α a), f (λ (i : ι), g i (r i)))

If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ..., `r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each coordinate. Here, we give an auxiliary statement tailored for an inductive proof. Use instead `map_sum_finset`.

theorem multilinear_map.map_sum_finset {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) {α : ι Type u_1} (g : Π (i : ι), α i M₁ i) (A : Π (i : ι), finset (α i)) [decidable_eq ι] [fintype ι] :
f (λ (i : ι), (A i).sum (λ (j : α i), g i j)) = .sum (λ (r : Π (a : ι), α a), f (λ (i : ι), g i (r i)))

If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ..., `r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each coordinate.

theorem multilinear_map.map_sum {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) {α : ι Type u_1} (g : Π (i : ι), α i M₁ i) [decidable_eq ι] [fintype ι] [Π (i : ι), fintype (α i)] :
f (λ (i : ι), finset.univ.sum (λ (j : α i), g i j)) = finset.univ.sum (λ (r : Π (i : ι), α i), f (λ (i : ι), g i (r i)))

If `f` is multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from multilinearity by expanding successively with respect to each coordinate.

theorem multilinear_map.map_update_sum {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) {α : Type u_1} [decidable_eq ι] (t : finset α) (i : ι) (g : α M₁ i) (m : Π (i : ι), M₁ i) :
f i (t.sum (λ (a : α), g a))) = t.sum (λ (a : α), f i (g a)))
@[simp]
theorem multilinear_map.cod_restrict_apply_coe {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) (p : M₂) (h : (v : Π (i : ι), M₁ i), f v p) (v : Π (i : ι), M₁ i) :
((f.cod_restrict p h) v) = f v
def multilinear_map.cod_restrict {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) (p : M₂) (h : (v : Π (i : ι), M₁ i), f v p) :
M₁ p

Restrict the codomain of a multilinear map to a submodule.

This is the multilinear version of `linear_map.cod_restrict`.

Equations
def multilinear_map.restrict_scalars (R : Type u) {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {A : Type u_1} [semiring A] [ A] [Π (i : ι), (M₁ i)] [ M₂] [ (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) :
M₁ M₂

Reinterpret an `A`-multilinear map as an `R`-multilinear map, if `A` is an algebra over `R` and their actions on all involved modules agree with the action of `R` on `A`.

Equations
@[simp]
theorem multilinear_map.coe_restrict_scalars (R : Type u) {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {A : Type u_1} [semiring A] [ A] [Π (i : ι), (M₁ i)] [ M₂] [ (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) :
def multilinear_map.dom_dom_congr {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : (λ (i : ι₁), M₂) M₃) :
(λ (i : ι₂), M₂) M₃

Transfer the arguments to a map along an equivalence between argument indices.

The naming is derived from `finsupp.dom_congr`, noting that here the permutation applies to the domain of the domain.

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_apply {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : (λ (i : ι₁), M₂) M₃) (v : ι₂ M₂) :
= m (λ (i : ι₁), v (σ i))
theorem multilinear_map.dom_dom_congr_trans {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (σ₁ : ι₁ ι₂) (σ₂ : ι₂ ι₃) (m : (λ (i : ι₁), M₂) M₃) :
theorem multilinear_map.dom_dom_congr_mul {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} (σ₁ σ₂ : equiv.perm ι₁) (m : (λ (i : ι₁), M₂) M₃) :
@[simp]
theorem multilinear_map.dom_dom_congr_equiv_apply {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : (λ (i : ι₁), M₂) M₃) :
def multilinear_map.dom_dom_congr_equiv {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
(λ (i : ι₁), M₂) M₃ ≃+ (λ (i : ι₂), M₂) M₃

`multilinear_map.dom_dom_congr` as an equivalence.

This is declared separately because it does not work with dot notation.

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_equiv_symm_apply {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : (λ (i : ι₂), M₂) M₃) :
@[simp]
theorem multilinear_map.dom_dom_congr_eq_iff {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [ M₂] [ M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (f g : (λ (i : ι₁), M₂) M₃) :

The results of applying `dom_dom_congr` to two maps are equal if and only if those maps are.

def linear_map.comp_multilinear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] (g : M₂ →ₗ[R] M₃) (f : M₁ M₂) :
M₁ M₃

Composing a multilinear map with a linear map gives again a multilinear map.

Equations
@[simp]
theorem linear_map.coe_comp_multilinear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] (g : M₂ →ₗ[R] M₃) (f : M₁ M₂) :
@[simp]
theorem linear_map.comp_multilinear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] (g : M₂ →ₗ[R] M₃) (f : M₁ M₂) (m : Π (i : ι), M₁ i) :
@[simp]
theorem linear_map.subtype_comp_multilinear_map_cod_restrict {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) (p : M₂) (h : (v : Π (i : ι), M₁ i), f v p) :

The multilinear version of `linear_map.subtype_comp_cod_restrict`

@[simp]
theorem linear_map.comp_multilinear_map_cod_restrict {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), (M₁ i)] [ M₂] [ M₃] (g : M₂ →ₗ[R] M₃) (f : M₁ M₂) (p : M₃) (h : (c : M₂), g c p) :
= p _

The multilinear version of `linear_map.comp_cod_restrict`

@[simp]
theorem linear_map.comp_multilinear_map_dom_dom_congr {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} {M' : Type v'} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M'] [ M₂] [ M₃] [ M'] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (g : M₂ →ₗ[R] M₃) (f : (λ (i : ι₁), M') M₂) :
theorem multilinear_map.map_piecewise_smul {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (c : ι R) (m : Π (i : ι), M₁ i) (s : finset ι) :
f (s.piecewise (λ (i : ι), c i m i) m) = s.prod (λ (i : ι), c i) f m

If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear map is multiplied by `∏ i in s, c i`. This is mainly an auxiliary statement to prove the result when `s = univ`, given in `map_smul_univ`, although it can be useful in its own right as it does not require the index set `ι` to be finite.

theorem multilinear_map.map_smul_univ {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [fintype ι] (c : ι R) (m : Π (i : ι), M₁ i) :
f (λ (i : ι), c i m i) = finset.univ.prod (λ (i : ι), c i) f m

Multiplicativity of a multilinear map along all coordinates at the same time, writing `f (λi, c i • m i)` as `(∏ i, c i) • f m`.

@[simp]
theorem multilinear_map.map_update_smul {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] [fintype ι] (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (function.update (c m) i x) = c ^ - 1) f i x)
@[protected, instance]
def multilinear_map.distrib_mul_action {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [ M₂] [ R' M₂] :
M₁ M₂)
Equations
@[protected, instance]
def multilinear_map.module {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), (M₁ i)] [ M₂] [module R' M₂] [ R' M₂] :
module R' M₁ M₂)

The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise addition and scalar multiplication.

Equations
@[protected, instance]
def multilinear_map.no_zero_smul_divisors {ι : Type u'} {M₁ : ι Type v₁} {M₃ : Type v₃} [Π (i : ι), add_comm_monoid (M₁ i)] {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), (M₁ i)] [add_comm_monoid M₃] [module R' M₃] [ M₃] [ R' M₃] [ M₃] :
M₁ M₃)
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv_symm_apply (M₂ : Type v₂) (M₃ : Type v₃) [add_comm_monoid M₂] (R' : Type u_1) (A : Type u_2) [semiring R'] [semiring A] [ M₂] [add_comm_monoid M₃] [module R' M₃] [ M₃] [ R' M₃] {ι₁ : Type u_3} {ι₂ : Type u_4} (σ : ι₁ ι₂) (ᾰ : (λ (i : ι₂), M₂) M₃) :
A σ).symm) =
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv_apply (M₂ : Type v₂) (M₃ : Type v₃) [add_comm_monoid M₂] (R' : Type u_1) (A : Type u_2) [semiring R'] [semiring A] [ M₂] [add_comm_monoid M₃] [module R' M₃] [ M₃] [ R' M₃] {ι₁ : Type u_3} {ι₂ : Type u_4} (σ : ι₁ ι₂) (ᾰ : (λ (i : ι₁), M₂) M₃) :
A σ) =
def multilinear_map.dom_dom_congr_linear_equiv (M₂ : Type v₂) (M₃ : Type v₃) [add_comm_monoid M₂] (R' : Type u_1) (A : Type u_2) [semiring R'] [semiring A] [ M₂] [add_comm_monoid M₃] [module R' M₃] [ M₃] [ R' M₃] {ι₁ : Type u_3} {ι₂ : Type u_4} (σ : ι₁ ι₂) :
(λ (i : ι₁), M₂) M₃ ≃ₗ[R'] (λ (i : ι₂), M₂) M₃

`multilinear_map.dom_dom_congr` as a `linear_equiv`.

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv'_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {ι' : Type u_1} (σ : ι ι') (f : M₁ M₂) :
σ) f = {to_fun := f σ).symm), map_add' := _, map_smul' := _}
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv'_symm_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {ι' : Type u_1} (σ : ι ι') (f : (λ (i : ι'), M₁ ((σ.symm) i)) M₂) :
σ).symm) f = {to_fun := f σ), map_add' := _, map_smul' := _}
def multilinear_map.dom_dom_congr_linear_equiv' (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] {ι' : Type u_1} (σ : ι ι') :
M₁ M₂ ≃ₗ[R] (λ (i : ι'), M₁ ((σ.symm) i)) M₂

The dependent version of `multilinear_map.dom_dom_congr_linear_equiv`.

Equations
def multilinear_map.const_linear_equiv_of_is_empty (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [is_empty ι] :
M₂ ≃ₗ[R] M₁ M₂

The space of constant maps is equivalent to the space of maps that are multilinear with respect to an empty family.

Equations
@[simp]
theorem multilinear_map.const_linear_equiv_of_is_empty_symm_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [is_empty ι] (f : M₁ M₂) :
.symm) f = f 0
@[simp]
theorem multilinear_map.const_linear_equiv_of_is_empty_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [is_empty ι] (m : M₂) :
@[protected]
def multilinear_map.mk_pi_algebra (R : Type u) (ι : Type u') (A : Type u_1) [ A] [fintype ι] :
(λ (i : ι), A) A

Given an `R`-algebra `A`, `mk_pi_algebra` is the multilinear map on `A^ι` associating to `m` the product of all the `m i`.

See also `multilinear_map.mk_pi_algebra_fin` for a version that works with a non-commutative algebra `A` but requires `ι = fin n`.

Equations
@[simp]
theorem multilinear_map.mk_pi_algebra_apply {R : Type u} {ι : Type u'} {A : Type u_1} [ A] [fintype ι] (m : ι A) :
m = finset.univ.prod (λ (i : ι), m i)
@[protected]
def multilinear_map.mk_pi_algebra_fin (R : Type u) (n : ) (A : Type u_1) [semiring A] [ A] :
(λ (i : fin n), A) A

Given an `R`-algebra `A`, `mk_pi_algebra_fin` is the multilinear map on `A^n` associating to `m` the product of all the `m i`.

See also `multilinear_map.mk_pi_algebra` for a version that assumes `[comm_semiring A]` but works for `A^ι` with any finite type `ι`.

Equations
@[simp]
theorem multilinear_map.mk_pi_algebra_fin_apply {R : Type u} {n : } {A : Type u_1} [semiring A] [ A] (m : fin n A) :
theorem multilinear_map.mk_pi_algebra_fin_apply_const {R : Type u} {n : } {A : Type u_1} [semiring A] [ A] (a : A) :
(λ (_x : fin n), a) = a ^ n
def multilinear_map.smul_right {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ R) (z : M₂) :
M₁ M₂

Given an `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the map sending `m` to `f m • z`.

Equations
@[simp]
theorem multilinear_map.smul_right_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ R) (z : M₂) (m : Π (i : ι), M₁ i) :
(f.smul_right z) m = f m z
@[protected]
def multilinear_map.mk_pi_ring (R : Type u) (ι : Type u') {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] (z : M₂) :
(λ (i : ι), R) M₂

The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of all the `m i` (multiplied by a fixed reference element `z` in the target module). See also `mk_pi_algebra` for a more general version.

Equations
• = z
@[simp]
theorem multilinear_map.mk_pi_ring_apply {R : Type u} {ι : Type u'} {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] (z : M₂) (m : ι R) :
z) m = finset.univ.prod (λ (i : ι), m i) z
theorem multilinear_map.mk_pi_ring_apply_one_eq_self {R : Type u} {ι : Type u'} {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] (f : (λ (i : ι), R) M₂) :
(f (λ (i : ι), 1)) = f
theorem multilinear_map.mk_pi_ring_eq_iff {R : Type u} {ι : Type u'} {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] {z₁ z₂ : M₂} :
= z₁ = z₂
theorem multilinear_map.mk_pi_ring_zero {R : Type u} {ι : Type u'} {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] :
= 0
theorem multilinear_map.mk_pi_ring_eq_zero_iff {R : Type u} {ι : Type u'} {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] (z : M₂) :
= 0 z = 0
@[protected, instance]
def multilinear_map.has_neg {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] :
has_neg M₁ M₂)
Equations
@[simp]
theorem multilinear_map.neg_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) (m : Π (i : ι), M₁ i) :
(-f) m = -f m
@[protected, instance]
def multilinear_map.has_sub {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] :
has_sub M₁ M₂)
Equations
@[simp]
theorem multilinear_map.sub_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] (f g : M₁ M₂) (m : Π (i : ι), M₁ i) :
(f - g) m = f m - g m
@[protected, instance]
def multilinear_map.add_comm_group {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] :
Equations
@[simp]
theorem multilinear_map.map_neg {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x : M₁ i) :
f i (-x)) = -f i x)
@[simp]
theorem multilinear_map.map_sub {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), (M₁ i)] [ M₂] (f : M₁ M₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i) :
f i (x - y)) = f i x) - f i y)
@[protected]
def multilinear_map.pi_ring_equiv {R : Type u} {ι : Type u'} {M₂ : Type v₂} [add_comm_monoid M₂] [ M₂] [fintype ι] :
M₂ ≃ₗ[R] (λ (i : ι), R) M₂

When `ι` is finite, multilinear maps on `R^ι` with values in `M₂` are in bijection with `M₂`, as such a multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear equivalence in `multilinear_map.pi_ring_equiv`.

Equations

### Currying #

We associate to a multilinear map in `n+1` variables (i.e., based on `fin n.succ`) two curried functions, named `f.curry_left` (which is a linear map on `E 0` taking values in multilinear maps in `n` variables) and `f.curry_right` (wich is a multilinear map in `n` variables taking values in linear maps on `E 0`). In both constructions, the variable that is singled out is `0`, to take advantage of the operations `cons` and `tail` on `fin n`. The inverse operations are called `uncurry_left` and `uncurry_right`.

We also register linear equiv versions of these correspondences, in `multilinear_curry_left_equiv` and `multilinear_curry_right_equiv`.

#### Left currying #

def linear_map.uncurry_left {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M 0 →ₗ[R] (λ (i : fin n), M i.succ) M₂) :
M₂

Given a linear map `f` from `M 0` to multilinear maps on `n` variables, construct the corresponding multilinear map on `n+1` variables obtained by concatenating the variables, given by `m ↦ f (m 0) (tail m)`

Equations
@[simp]
theorem linear_map.uncurry_left_apply {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M 0 →ₗ[R] (λ (i : fin n), M i.succ) M₂) (m : Π (i : fin n.succ), M i) :
(f.uncurry_left) m = (f (m 0)) (fin.tail m)
def multilinear_map.curry_left {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) :
M 0 →ₗ[R] (λ (i : fin n), M i.succ) M₂

Given a multilinear map `f` in `n+1` variables, split the first variable to obtain a linear map into multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`.

Equations
@[simp]
theorem multilinear_map.curry_left_apply {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) (x : M 0) (m : Π (i : fin n), M i.succ) :
((f.curry_left) x) m = f (fin.cons x m)
@[simp]
theorem linear_map.curry_uncurry_left {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M 0 →ₗ[R] (λ (i : fin n), M i.succ) M₂) :
@[simp]
theorem multilinear_map.uncurry_curry_left {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) :
def multilinear_curry_left_equiv (R : Type u) {n : } (M : fin n.succ Type v) (M₂ : Type v₂) [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] :
(M 0 →ₗ[R] (λ (i : fin n), M i.succ) M₂) ≃ₗ[R] M₂

The space of multilinear maps on `Π(i : fin (n+1)), M i` is canonically isomorphic to the space of linear maps from `M 0` to the space of multilinear maps on `Π(i : fin n), M i.succ`, by separating the first variable. We register this isomorphism as a linear isomorphism in `multilinear_curry_left_equiv R M M₂`.

The direct and inverse maps are given by `f.uncurry_left` and `f.curry_left`. Use these unless you need the full framework of linear equivs.

Equations

#### Right currying #

def multilinear_map.uncurry_right {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : (λ (i : fin n), M (fin.cast_succ i)) (M (fin.last n) →ₗ[R] M₂)) :
M₂

Given a multilinear map `f` in `n` variables to the space of linear maps from `M (last n)` to `M₂`, construct the corresponding multilinear map on `n+1` variables obtained by concatenating the variables, given by `m ↦ f (init m) (m (last n))`

Equations
@[simp]
theorem multilinear_map.uncurry_right_apply {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : (λ (i : fin n), M (fin.cast_succ i)) (M (fin.last n) →ₗ[R] M₂)) (m : Π (i : fin n.succ), M i) :
def multilinear_map.curry_right {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) :
(λ (i : fin n), M (fin.cast_succ i)) (M (fin.last n) →ₗ[R] M₂)

Given a multilinear map `f` in `n+1` variables, split the last variable to obtain a multilinear map in `n` variables taking values in linear maps from `M (last n)` to `M₂`, given by `m ↦ (x ↦ f (snoc m x))`.

Equations
@[simp]
theorem multilinear_map.curry_right_apply {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) (m : Π (i : fin n), M ) (x : M (fin.last n)) :
((f.curry_right) m) x = f (fin.snoc m x)
@[simp]
theorem multilinear_map.curry_uncurry_right {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : (λ (i : fin n), M (fin.cast_succ i)) (M (fin.last n) →ₗ[R] M₂)) :
@[simp]
theorem multilinear_map.uncurry_curry_right {R : Type u} {n : } {M : fin n.succ Type v} {M₂ : Type v₂} [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] (f : M₂) :
def multilinear_curry_right_equiv (R : Type u) {n : } (M : fin n.succ Type v) (M₂ : Type v₂) [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), (M i)] [ M₂] :
(λ (i : fin n), M (fin.cast_succ i)) (M (fin.last n) →ₗ[R] M₂) ≃ₗ[R] M₂

The space of multilinear maps on `Π(i : fin (n+1)), M i` is canonically isomorphic to the space of linear maps from the space of multilinear maps on `Π(i : fin n), M i.cast_succ` to the space of linear maps on `M (last n)`, by separating the last variable. We register this isomorphism as a linear isomorphism in `multilinear_curry_right_equiv R M M₂`.

The direct and inverse maps are given by `f.uncurry_right` and `f.curry_right`. Use these unless you need the full framework of linear equivs.

Equations
def multilinear_map.curry_sum {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {ι' : Type u_1} (f : (λ (x : ι ι'), M') M₂) :
(λ (x : ι), M') (λ (x : ι'), M') M₂)

A multilinear map on `Π i : ι ⊕ ι', M'` defines a multilinear map on `Π i : ι, M'` taking values in the space of multilinear maps on `Π i : ι', M'`.

Equations
@[simp]
theorem multilinear_map.curry_sum_apply {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {ι' : Type u_1} (f : (λ (x : ι ι'), M') M₂) (u : ι M') (v : ι' M') :
((f.curry_sum) u) v = f (sum.elim u v)
def multilinear_map.uncurry_sum {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {ι' : Type u_1} (f : (λ (x : ι), M') (λ (x : ι'), M') M₂)) :
(λ (x : ι ι'), M') M₂

A multilinear map on `Π i : ι, M'` taking values in the space of multilinear maps on `Π i : ι', M'` defines a multilinear map on `Π i : ι ⊕ ι', M'`.

Equations
@[simp]
theorem multilinear_map.uncurry_sum_aux_apply {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {ι' : Type u_1} (f : (λ (x : ι), M') (λ (x : ι'), M') M₂)) (u : ι ι' M') :
def multilinear_map.curry_sum_equiv (R : Type u) (ι : Type u') (M₂ : Type v₂) (M' : Type v') [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] (ι' : Type u_1) :
(λ (x : ι ι'), M') M₂ ≃ₗ[R] (λ (x : ι), M') (λ (x : ι'), M') M₂)

Linear equivalence between the space of multilinear maps on `Π i : ι ⊕ ι', M'` and the space of multilinear maps on `Π i : ι, M'` taking values in the space of multilinear maps on `Π i : ι', M'`.

Equations
@[simp]
theorem multilinear_map.coe_curry_sum_equiv {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {ι' : Type u_1} :
@[simp]
theorem multilinear_map.coe_curr_sum_equiv_symm {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {ι' : Type u_1} :
def multilinear_map.curry_fin_finset (R : Type u) (M₂ : Type v₂) (M' : Type v') [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) :
(λ (x : fin n), M') M₂ ≃ₗ[R] (λ (x : fin k), M') (λ (x : fin l), M') M₂)

If `s : finset (fin n)` is a finite set of cardinality `k` and its complement has cardinality `l`, then the space of multilinear maps on `λ i : fin n, M'` is isomorphic to the space of multilinear maps on `λ i : fin k, M'` taking values in the space of multilinear maps on `λ i : fin l, M'`.

Equations
@[simp]
theorem multilinear_map.curry_fin_finset_apply {R : Type u} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (x : fin n), M') M₂) (mk : fin k M') (ml : fin l M') :
(( M' hk hl) f) mk) ml = f (λ (i : fin n), sum.elim mk ml ( hl).symm) i))
@[simp]
theorem multilinear_map.curry_fin_finset_symm_apply {R : Type u} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (x : fin k), M') (λ (x : fin l), M') M₂)) (m : fin n M') :
( M' hk hl).symm) f) m = (f (λ (i : fin k), m ( hl) (sum.inl i)))) (λ (i : fin l), m ( hl) (sum.inr i)))
@[simp]
theorem multilinear_map.curry_fin_finset_symm_apply_piecewise_const {R : Type u} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (x : fin k), M') (λ (x : fin l), M') M₂)) (x y : M') :
( M' hk hl).symm) f) (s.piecewise (λ (_x : fin n), x) (λ (_x : fin n), y)) = (f (λ (_x : fin k), x)) (λ (_x : fin l), y)
@[simp]
theorem multilinear_map.curry_fin_finset_symm_apply_const {R : Type u} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (x : fin k), M') (λ (x : fin l), M') M₂)) (x : M') :
( M' hk hl).symm) f) (λ (_x : fin n), x) = (f (λ (_x : fin k), x)) (λ (_x : fin l), x)
@[simp]
theorem multilinear_map.curry_fin_finset_apply_const {R : Type u} {M₂ : Type v₂} {M' : Type v'} [add_comm_monoid M'] [add_comm_monoid M₂] [ M'] [ M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : (λ (x : fin n), M') M₂) (x y : M') :
(( M' hk hl) f) (λ (_x : fin k), x)) (λ (_x : fin l), y) = f (s.piecewise (λ (_x : fin n), x) (λ (_x : fin n), y))
def multilinear_map.map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [nonempty ι] (f : M₁ M₂) (p : Π (i : ι), (M₁ i)) :
M₂

The pushforward of an indexed collection of submodule `p i ⊆ M₁ i` by `f : M₁ → M₂`.

Note that this is not a submodule - it is not closed under addition.

Equations
theorem multilinear_map.map_nonempty {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [nonempty ι] (f : M₁ M₂) (p : Π (i : ι), (M₁ i)) :

The map is always nonempty. This lemma is needed to apply `sub_mul_action.zero_mem`.

def multilinear_map.range {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), (M₁ i)] [ M₂] [nonempty ι] (f : M₁ M₂) :
M₂

The range of a multilinear map, closed under scalar multiplication.

Equations