Theorems · Definition · linear algebra
MultilinearMap.toFun
{R : Type uR} →
{ι : Type uι} →
{M₁ : ι → Type v₁} →
{M₂ : Type v₂} →
[inst : Semiring R] →
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
[inst_2 : AddCommMonoid M₂] →
[inst_3 : (i : ι) → Module R (M₁ i)] →
[inst_4 : Module R M₂] → MultilinearMap R M₁ M₂ → ((i : ι) → M₁ i) → M₂The underlying multivariate function of a multilinear map.
- Defined in
- Mathlib.LinearAlgebra.Multilinear.Basic
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- MultilinearMapstatement and proof · cited by 370
Cited by38
Results whose statement or proof uses this declaration.
- ContinuousMultilinearMap.contstatement · cited by 6
- ContinuousMultilinearMap.toMultilinearMap_injectiveproof · cited by 5
- MultilinearMap.map_update_add'statement · cited by 4
- MultilinearMap.map_update_smul'statement · cited by 4
- AlternatingMap.map_eq_zero_of_eq'statement · cited by 3
- ContinuousAlternatingMap.map_eq_zero_of_eq'statement · cited by 2
- ContinuousMultilinearMap.mk.injstatement and proof · cited by 1
- ContinuousMultilinearMap.mk.noConfusionstatement and proof · cited by 1
- ContinuousAlternatingMap.toContinuousMultilinearMap_injectiveproof · cited by 1
- AlternatingMap.mk.congr_simpstatement and proof · cited by 1
- AlternatingMap.mk.injstatement and proof · cited by 1
- AlternatingMap.mk.noConfusionstatement and proof · cited by 1