constVAddHom — Mathlib

English

ConstVAddHom is a MonoidHom from Multiplicative G to Equiv.Perm P, sending v to constVAdd P (v.toAdd).

Русский

ConstVAddHom — моноидоморфизм от Multiplicative G к Equiv.Perm P, отображающий v в constVAdd P (v.toAdd).

LaTeX

$$$$ \text{constVAddHom} : \text{Multiplicative } G \rightarrow* \text{Equiv.Perm } P, \quad \text{toFun}(v) = \text{constVAdd } P (v^{\text{toAdd}}) $$$$

Lean4

/-- `Equiv.constVAdd` as a homomorphism from `Multiplicative G` to `Equiv.perm P` -/
def constVAddHom : Multiplicative G →* Equiv.Perm P
    where
  toFun v := constVAdd P (v.toAdd)
  map_one' := constVAdd_zero G P
  map_mul' := constVAdd_add P

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