algEquiv — Mathlib

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 _

Похожие утверждения