unitizationAlgEquiv — Mathlib

English

There exists an algebra isomorphism (over any suitable R) between WithLp 1 (Unitization 𝕜 A) and Unitization 𝕜 A.

Русский

Существует алгебраическое изоморфизм между WithLp 1 (Unitization 𝕜 A) и Unitization 𝕜 A.

LaTeX

$$WithLp.unitizationAlgEquiv R : WithLp 1 (Unitization 𝕜 A) ≃ₐ[R] Unitization 𝕜 A$$

Lean4

/-- `equiv` bundled as an algebra isomorphism with `Unitization 𝕜 A`. -/
@[simps!]
def unitizationAlgEquiv (R : Type*) [CommSemiring R] [Algebra R 𝕜] [DistribMulAction R A] [IsScalarTower R 𝕜 A] :
    WithLp 1 (Unitization 𝕜 A) ≃ₐ[R] Unitization 𝕜 A
    where
  __ := WithLp.linearEquiv _ R _
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
  commutes' _ := rfl

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