English
A construction that combines a linear equivalence with a cast yields a larger equivalence with explicit components.
Русский
Построение, объединяющее линейное эквивалентность с cast, образует более крупную эквивалентность с явными компонентами.
LaTeX
$$mk_cast : (e, cast) → M ≃ₗ M'$$
Lean4
/-- `Equiv.cast (congrArg _ h)` as a linear equiv.
Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself. -/
@[simps!]
protected def cast {ι : Type*} {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] {i j : ι} (h : i = j) :
M i ≃ₗ[R] M j where
toAddEquiv := AddEquiv.cast h
map_smul' _ _ := by cases h; rfl
