instAddConstMapClass — Mathlib

English

There is a canonical AddConstMapClass structure on AddConstEquiv G H a b; in other words, AddConstEquiv objects carry a natural AddConstMapClass structure between G and H with constants a and b.

Русский

Существует каноническая структура AddConstMapClass на AddConstEquiv G H a b; то есть объекты AddConstEquiv естественным образом образуют структуру AddConstMapClass между G и H с константами a и b.

LaTeX

$$$ \text{AddConstMapClass}(\text{AddConstEquiv } G H a b) G H a b $$$$

Lean4

instance {G H : Type*} [Add G] [Add H] {a : G} {b : H} : AddConstMapClass (G ≃+c[a, b] H) G H a b where
  map_add_const f x := f.map_add_const' x

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