image_div — Mathlib

English

Let m be a monoid homomorphism and s, t subsets of the domain. Then the image of the quotient set s/t equals the quotient of the images: m[s/t] = m[s]/m[t].

Русский

Пусть m — гомоморфизм моноидов и s, t — множества в области определения. Тогда образ множества деления равен делению образов: m[s/t] = m[s]/m[t].

LaTeX

$$$m[S/T] = m[S]/m[T]$$$

Lean4

@[to_additive]
theorem image_div : m '' (s / t) = m '' s / m '' t :=
  image_image2_distrib <| map_div m

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