LinearEquiv.prodCongrRight

Stream: Is there code for X?

[Kevin Buzzard]

Do we really not have this? I've tried exact? and loogle but would be shocked if it really is missing.

import Mathlib

open TensorProduct

def LinearEquiv.prodCongrRight (R M N P : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P]
    (e : N ≃ₗ[R] P) : (M × N) ≃ₗ[R] (M × P) where
  toFun mn := (mn.1, e mn.2)
  map_add' _ _ := by simp
  map_smul' _ _ := by simp
  invFun mp := (mp.1, e.symm mp.2)
  left_inv _ := by simp
  right_inv _ := by simp

I can't even find AddEquiv.prodCongrRight. We do have docs#Equiv.prodCongrRight but it's slightly different because it allows dependent equivs.

[Kevin Buzzard]

Oh I see, I guess I just use docs#LinearEquiv.prodCongr