equiv — Mathlib

English

There is a canonical equivalence between WithCStarModule A E and E, given by the identity.

Русский

Существует каноническое эквивалентность между WithCStarModule A E и E, задаваемая тождеством.

LaTeX

$$$WithCStarModule(A,E) \\simeq E\\; (\\text{canonical, identity})$$$

Lean4

/-- The canonical equivalence between `C⋆ᵐᵒᵈ(A, E)` and `E`. This should always be used to
convert back and forth between the representations. -/
def equiv : WithCStarModule A E ≃ E :=
  Equiv.refl _

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