gcd_congr

Mathlib.Algebra.GCDMonoid.Finset

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

English

If s1 = s2 and f equals g on s2, then s1.gcd f = s2.gcd g.

Русский

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

LaTeX

$$$(s_1 = s_2) \Rightarrow (s_1.gcd f = s_2.gcd g)$ with $\forall a \in s_2, f(a)=g(a)$$$

Lean4

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

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

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

Разделы

Аффилиация

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