map — Mathlib

English

If f: M → N is a monoid hom, and x ~ᵤ y in M, then f(x) ~ᵤ f(y) in N.

Русский

Если f: M → N — гомоморф моноидов, и x ~ᵤ y в M, то f(x) ~ᵤ f(y) в N.

LaTeX

$$$\\text{Associated}(x,y) \\Rightarrow \\text{Associated}(f(x), f(y))$$$

Lean4

theorem map {M N : Type*} [Monoid M] [Monoid N] {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) {x y : M}
    (ha : Associated x y) : Associated (f x) (f y) :=
  by
  obtain ⟨u, ha⟩ := ha
  exact ⟨Units.map f u, by rw [← ha, map_mul, Units.coe_map, MonoidHom.coe_coe]⟩

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