lcm_congr

Mathlib.Algebra.GCDMonoid.Finset

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

English

If s1 = s2 and f and g agree on s2, then s1.lcm f = s2.lcm g.

Русский

Если s1 = s2 и f(a) = g(a) для всех a∈s2, то s1.lcm f = s2.lcm g.

LaTeX

$$$(s_1 = s_2) \Rightarrow (s_1.lcm f = s_2.lcm g) \quad \text{if } (\forall a \in s_2,\ f(a)=g(a))$$$

Lean4

theorem lcm_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) : s₁.lcm f = s₂.lcm g :=
  by
  subst hs
  exact Finset.fold_congr hfg

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

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

Разделы

Аффилиация

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