From d7b5ffa00983f5d9c8fcb914d0d94019a51d6e6b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 12 Nov 2021 15:38:33 +0000
Subject: [PATCH] chore(linear_algebra/multilinear): add const_of_is_empty
 (#10291)

This is extracted from `pi_tensor_product.is_empty_equiv`
---
 src/linear_algebra/multilinear/basic.lean | 9 +++++++++
 src/linear_algebra/pi_tensor_product.lean | 4 ++--
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/linear_algebra/multilinear/basic.lean b/src/linear_algebra/multilinear/basic.lean
index 0b2e9306c5a13..903d4e42177cb 100644
--- a/src/linear_algebra/multilinear/basic.lean
+++ b/src/linear_algebra/multilinear/basic.lean
@@ -201,6 +201,15 @@ def of_subsingleton [subsingleton ι] (i' : ι) : multilinear_map R (λ _ : ι,
   map_smul' := λ m i r x, by {
     rw subsingleton.elim i i', simp only [function.eval, function.update_same], } }
 
+variables {M₂}
+
+/-- The constant map is multilinear when `ι` is empty. -/
+@[simps {fully_applied := ff}]
+def const_of_is_empty [is_empty ι] (m : M₂) : multilinear_map R M₁ M₂ :=
+{ to_fun := function.const _ m,
+  map_add' := λ m, is_empty_elim,
+  map_smul' := λ m, is_empty_elim }
+
 end
 
 /-- Given a multilinear map `f` on `n` variables (parameterized by `fin n`) and a subset `s` of `k`
diff --git a/src/linear_algebra/pi_tensor_product.lean b/src/linear_algebra/pi_tensor_product.lean
index c2314e9899dd4..05730550a322a 100644
--- a/src/linear_algebra/pi_tensor_product.lean
+++ b/src/linear_algebra/pi_tensor_product.lean
@@ -440,7 +440,7 @@ variables (ι)
 /-- The tensor product over an empty index type `ι` is isomorphic to the base ring. -/
 @[simps symm_apply]
 def is_empty_equiv [is_empty ι] : ⨂[R] i : ι, M ≃ₗ[R] R :=
-{ to_fun := lift ⟨λ (_ : ι → M), (1 : R), λ v, is_empty_elim, λ v, is_empty_elim⟩,
+{ to_fun := lift (const_of_is_empty R 1),
   inv_fun := λ r, r • tprod R (@is_empty_elim _ _ _),
   left_inv := λ x, by {
     apply x.induction_on,
@@ -450,7 +450,7 @@ def is_empty_equiv [is_empty ι] : ⨂[R] i : ι, M ≃ₗ[R] R :=
     { simp only,
       intros x y hx hy,
       simp [add_smul, hx, hy] }},
-  right_inv := λ t, by simp only [mul_one, algebra.id.smul_eq_mul, multilinear_map.coe_mk,
+  right_inv := λ t, by simp only [mul_one, algebra.id.smul_eq_mul, const_of_is_empty_apply,
     linear_map.map_smul, pi_tensor_product.lift.tprod],
   map_add' := linear_map.map_add _,
   map_smul' := linear_map.map_smul _, }