lcm_eq_lcm_image

Mathlib.Algebra.GCDMonoid.Finset

URI: https://scilib.ai/kg/mathlib#Finset.lcm_eq_lcm_image

English

For s with a decidable equality on α, the lcm over s with f equals the lcm of the image of s under f with id.

Русский

Для s c разрешимой эквивалентностью на α НОК над s и f равен НОК образа s через f и идентичность.

LaTeX

$$$s.lcm f = (s.image f).lcm id$$$

Lean4

theorem lcm_eq_lcm_image [DecidableEq α] : s.lcm f = (s.image f).lcm id :=
  Eq.symm <| lcm_image _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru