mulOneClass — Mathlib

English

Let e: α ≃ β. If β has a MulOneClass, then α inherits a MulOneClass via the transported multiplication.

Русский

Пусть e: α ≃ β. Если β обладает MulOneClass, то α наследует MulOneClass через перенесённое умножение.

LaTeX

$$$\text{MulOneClass}_\alpha \text{ with } a \star b := e^{-1}(e(a)\cdot e(b))$$$

Lean4

/-- Transfer `MulOneClass` across an `Equiv` -/
@[to_additive /-- Transfer `AddZeroClass` across an `Equiv` -/
    ]
protected abbrev mulOneClass [MulOneClass β] : MulOneClass α :=
  by
  let one := e.one
  let mul := e.mul
  apply e.injective.mulOneClass _ <;> intros <;> exact e.apply_symm_apply _

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