lcm_image — Mathlib

English

For s ⊆ γ and g: γ → β, the lcm of the image of s under g with respect to f equals the lcm of s under f ∘ g.

Русский

Для s ⊆ γ и отображения g: γ → β, НОК образа s по g относительно f равен НОК через композицию f ∘ g по s.

LaTeX

$$$ (s.\mathrm{image} g).lcm f = s.lcm (f \circ g) $$$

Lean4

theorem lcm_image [DecidableEq β] {g : γ → β} (s : Finset γ) : (s.image g).lcm f = s.lcm (f ∘ g) := by
  classical induction s using Finset.induction <;> simp [*]

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