finsetIntegerMultiple_image — Mathlib

English

The image of the finset of numerators under algebraMap equals the common denominator times the set s.

Русский

Образ числителей через алгебраическое отображение равен общему знаменателю, умноженному на множество s.

LaTeX

$$$\text{algebraMap } R S '' \text{finsetIntegerMultiple }(M,s) = \text{commonDenomOfFinset }(M,s) \cdot (s:\text{Set} S)$$$

Lean4

theorem finsetIntegerMultiple_image [DecidableEq R] (s : Finset S) :
    algebraMap R S '' finsetIntegerMultiple M s = commonDenomOfFinset M s • (s : Set S) :=
  by
  delta finsetIntegerMultiple commonDenom
  rw [Finset.coe_image]
  ext
  constructor
  · rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
    rw [map_integerMultiple]
    exact Set.mem_image_of_mem _ x.prop
  · rintro ⟨x, hx, rfl⟩
    exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩

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