lcm_insert — Mathlib

English

Let s be a finite set of indices and b an index. The lcm over the union of {b} and s equals the lcm of f(b) and the lcm over s.

Русский

Пусть s — конечное множество индексов и b индекс. НОК по объединению {b} и s равен НОК f(b) и НОК по s.

LaTeX

$$$((\mathrm{insert}\; b\; s).lcm f) = \operatorname{lcm}(f(b), s.lcm f)$$$

Lean4

@[simp]
theorem lcm_insert [DecidableEq β] {b : β} : (insert b s : Finset β).lcm f = GCDMonoid.lcm (f b) (s.lcm f) :=
  by
  by_cases h : b ∈ s
  · rw [insert_eq_of_mem h, (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
  apply fold_insert h

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