feat(linear_algebra/alternating): add 3 missing definitions (#19069)

src/linear_algebra/alternating.lean

@@ -51,6 +51,7 @@ using `map_swap` as a definition, and does not require `has_neg N`.
 variables {R : Type*} [semiring R]
 variables {M : Type*} [add_comm_monoid M] [module R M]
 variables {N : Type*} [add_comm_monoid N] [module R N]
+variables {P : Type*} [add_comm_monoid P] [module R P]
 
 -- semiring / add_comm_group
 variables {M' : Type*} [add_comm_group M'] [module R M']
@@ -207,6 +208,49 @@ instance [distrib_mul_action Sᵐᵒᵖ N] [is_central_scalar S N] :
 
 end has_smul
 
+/-- The cartesian product of two alternating maps, as a multilinear map. -/
+@[simps { simp_rhs := tt }]
+def prod (f : alternating_map R M N ι) (g : alternating_map R M P ι) :
+  alternating_map R M (N × P) ι :=
+{ map_eq_zero_of_eq' := λ v i j h hne, prod.ext (f.map_eq_zero_of_eq _ h hne)
+    (g.map_eq_zero_of_eq _ h hne),
+  .. f.to_multilinear_map.prod g.to_multilinear_map }
+
+@[simp]
+lemma coe_prod (f : alternating_map R M N ι) (g : alternating_map R M P ι) :
+  (f.prod g : multilinear_map R (λ _ : ι, M) (N × P)) = multilinear_map.prod f g :=
+rfl
+
+/-- Combine a family of alternating maps with the same domain and codomains `N i` into an
+alternating map taking values in the space of functions `Π i, N i`. -/
+@[simps { simp_rhs := tt }]
+def pi {ι' : Type*} {N : ι' → Type*} [∀ i, add_comm_monoid (N i)] [∀ i, module R (N i)]
+  (f : ∀ i, alternating_map R M (N i) ι) : alternating_map R M (∀ i, N i) ι :=
+{ map_eq_zero_of_eq' := λ v i j h hne, funext $ λ a, (f a).map_eq_zero_of_eq _ h hne,
+  .. multilinear_map.pi (λ a, (f a).to_multilinear_map) }
+
+@[simp]
+lemma coe_pi {ι' : Type*} {N : ι' → Type*} [∀ i, add_comm_monoid (N i)]
+  [∀ i, module R (N i)] (f : ∀ i, alternating_map R M (N i) ι) :
+  (pi f : multilinear_map R (λ _ : ι, M) (∀ i, N i)) = multilinear_map.pi (λ a, f a) :=
+rfl
+
+/-- Given an alternating `R`-multilinear map `f` taking values in `R`, `f.smul_right z` is the map
+sending `m` to `f m • z`. -/
+@[simps { simp_rhs := tt }]
+def smul_right {R M₁ M₂ ι : Type*} [comm_semiring R]
+  [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂]
+  (f : alternating_map R M₁ R ι) (z : M₂) : alternating_map R M₁ M₂ ι :=
+{ map_eq_zero_of_eq' := λ v i j h hne, by simp [f.map_eq_zero_of_eq v h hne],
+  .. f.to_multilinear_map.smul_right z }
+
+@[simp]
+lemma coe_smul_right {R M₁ M₂ ι : Type*} [comm_semiring R]
+  [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂]
+  (f : alternating_map R M₁ R ι) (z : M₂) :
+  (f.smul_right z : multilinear_map R (λ _ : ι, M₁) M₂) = multilinear_map.smul_right f z :=
+rfl
+
 instance : has_add (alternating_map R M N ι) :=
 ⟨λ a b,
   { map_eq_zero_of_eq' :=
@@ -335,6 +379,12 @@ def comp_alternating_map (g : N →ₗ[R] N₂) : alternating_map R M N ι →+
 lemma comp_alternating_map_apply (g : N →ₗ[R] N₂) (f : alternating_map R M N ι) (m : ι → M) :
   g.comp_alternating_map f m = g (f m) := rfl
 
+lemma smul_right_eq_comp {R M₁ M₂ ι : Type*} [comm_semiring R]
+  [add_comm_monoid M₁] [add_comm_monoid M₂] [module R M₁] [module R M₂]
+  (f : alternating_map R M₁ R ι) (z : M₂) :
+  f.smul_right z = (linear_map.id.smul_right z).comp_alternating_map f :=
+rfl
+
 @[simp]
 lemma subtype_comp_alternating_map_cod_restrict (f : alternating_map R M N ι) (p : submodule R N)
   (h) :

src/linear_algebra/multilinear/basic.lean

@@ -206,7 +206,7 @@ coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate. -/
   map_smul' := λc x, by simp }
 
 /-- The cartesian product of two multilinear maps, as a multilinear map. -/
-def prod (f : multilinear_map R M₁ M₂) (g : multilinear_map R M₁ M₃) :
+@[simps] def prod (f : multilinear_map R M₁ M₂) (g : multilinear_map R M₁ M₃) :
   multilinear_map R M₁ (M₂ × M₃) :=
 { to_fun    := λ m, (f m, g m),
   map_add'  := λ _ m i x y, by simp,