map_mabs — Mathlib

English

If f is order-preserving and monoid-homomorphic, then f(|a|_m) = |f(a)|_m.

Русский

Если f является порядок‑гомоморфизмом между группами, то f(|a|_m) = |f(a)|_m.

LaTeX

$$$f(|a|_m) = |f(a)|_m$$$

Lean4

@[to_additive (attr := simp)]
theorem map_mabs {β F : Type*} [Group β] [LinearOrder β] [FunLike F α β] [OrderHomClass F α β] [MonoidHomClass F α β]
    (f : F) (a : α) : f |a|ₘ = |f a|ₘ := by rw [mabs, mabs, (OrderHomClass.mono f).map_max, map_inv]

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