LinearEquiv.cast / AddEquiv.cast etc

Stream: Is there code for X?

[Eric Wieser]

We have docs#Equiv.cast; do we have anything along the lines of the following?

import Mathlib

@[simps]
def LinearEquiv.cast
    {ι} (R) {M : ι → Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
    {i j : ι} (h : i = j) :
    M i ≃ₗ[R] M j where
  __ := Equiv.cast (congrArg _ h)
  map_add' _ _ := by cases h; rfl
  map_smul' _ _ := by cases h; rfl

(and AddEquiv.cast / MulEquiv.cast / AlgEquiv.cast / AffineEquiv.cast / ContinuousLinearEquiv.cast)

[Eric Wieser]

docs#LinearEquiv.ofEq is close, in that in a special case they are equal:

example {R M} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p q : Submodule R M) (h : p = q) :
    LinearEquiv.ofEq p q h = LinearEquiv.cast R (M := fun p : Submodule R M => ↥p) h := by
  cases h
  rfl

[Eric Wieser]

Aha, #mathlib4 > Equiv.cast for structures @ 💬