map_units_inv — Mathlib

English

For any f : F with FunLike M α and a Units M u, the map f on u⁻¹ equals the inverse of f on u, i.e., f(u⁻¹) = f(u)⁻¹.

Русский

Для любого f с FunLike M α и единицы u в M верно f(u⁻¹) = f(u)⁻¹.

LaTeX

$$$f(\\uparrow u^{-1}) = (f u)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.map_units_inv {F : Type*} [FunLike F M α] [MonoidHomClass F M α] (f : F) (u : Units M) :
    f ↑u⁻¹ = (f u)⁻¹ :=
  ((f : M →* α).comp (Units.coeHom M)).map_inv u

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