toHomUnitsMulEquiv — Mathlib

English

There is a multiplicative equivalence between MonoidHom G M and MonoidHom G Mˣ, i.e., MonoidHom G M ≃* MonoidHom G Mˣ.

Русский

Существует мультипликативное эквидивное соответствие между MonoidHom G M и MonoidHom G Mˣ: MonoidHom G M ≃* MonoidHom G Mˣ.

LaTeX

$$$\\text{MonoidHom}(G,M) \\simeq_{\\mathrm{Mul}} \\text{MonoidHom}(G,M^{\\times}).$$$

Lean4

/-- `MonoidHom.toHomUnits` as a `MulEquiv`. -/
@[simps]
def toHomUnitsMulEquiv : (G →* M) ≃* (G →* Mˣ) where
  toFun := toHomUnits
  invFun f := (Units.coeHom _).comp f
  map_mul' := by simp

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