English
Shrinking a small algebra preserves algebra structure via an algebra isomorphism Shrink α ≃ₐ[R] α; i.e., shrinking does not change the algebra up to isomorphism.
Русский
Сужение малой алгебры сохраняет алгебраическую структуру через алгебраическое изоморфизм Shrink α ≃ₐ[R] α.
LaTeX
$$$\mathrm{Shrink}.\mathrm{algEquiv}_{R,\alpha}: \mathrm{Shrink}(\alpha) \simeq_{\mathrm{Alg}_R} \alpha$$$
Lean4
/-- Shrinking `α` to a smaller universe preserves algebra structure. -/
@[simps!]
def algEquiv [Small.{v} α] [Semiring α] [Algebra R α] : Shrink.{v} α ≃ₐ[R] α :=
(equivShrink α).symm.algEquiv _