instStarHomClass — Mathlib

English

Any class of star-ring equivalences between A and B yields a class of star-homomorphisms; i.e., they preserve addition, multiplication, and star.

Русский

Любой класс звездно-кольцевых эквивалентностей между A и B порождает класс звездоморфизмов; то есть сохраняют сумму, произведение и звездную операцию.

LaTeX

$$∀ f ∈ F, f ∈ \mathrm{StarHom}(A,B)$$

Lean4

instance (priority := 50) {F A B : Type*} [Add A] [Mul A] [Star A] [Add B] [Mul B] [Star B] [EquivLike F A B]
    [hF : StarRingEquivClass F A B] : StarHomClass F A B :=
  { hF with }
    -- See note [lower instance priority]

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