castHom — Mathlib

English

Let α be a DivisionRing of characteristic zero and s a multiset of rationals. Then the cast of the sum of s equals the sum of the casts of the elements.

Русский

Пусть α — делимое кольцо характеристика ноль, и s — мультисет рациональных чисел. Тогда приведение суммы s к α равно сумме приведённых элементов.

LaTeX

$$$ (\mathrm{sum}\, s)^{\uparrow} = \mathrm{sum}(\mathrm{map}(\uparrow)\, s). $$$

Lean4

/-- Coercion `ℚ → α` as a `RingHom`. -/
def castHom : ℚ →+* α where
  toFun := (↑)
  map_one' := cast_one
  map_mul' := cast_mul
  map_zero' := cast_zero
  map_add' := cast_add

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