map_integerMultiple — Mathlib

English

There exists a common denominator b such that its image under algebraMap, applied to the numerator, equals b times the fraction.

Русский

Существует общее знаменатель b, чья образ под algebraMap, примененный к числителю, равен b умножить на дробь.

LaTeX

$$$\exists b \in M, \ algebraMap(R,S)(\text{integerMultiple}(M,s,f,i)) = (b:R) \cdot f(i)$$$

Lean4

@[simp]
theorem map_integerMultiple {ι : Type*} (s : Finset ι) (f : ι → S) (i : s) :
    algebraMap R S (integerMultiple M s f i) = commonDenom M s f • f i :=
  ((exist_integer_multiples M s f).choose_spec _ i.prop).choose_spec

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