range_castAddHom — Mathlib

English

Let A be an additive group with one (AddGroupWithOne). Then the image of the integers under the canonical map Int.castAddHom A is exactly the subgroup zmultiples(1) in A (the set of all integer multiples of the unit).

Русский

Пусть A — аддитивная группа с единицей. Образ целых чисел под отображением Int.castAddHom A равен подгруппе zmultiples(1) в A. Это множество всех целочисленных кратных единице.

LaTeX

$$$\operatorname{range}(\mathrm{Int.castAddHom}\,A) = \operatorname{zmultiples}(1)$$$

Lean4

@[simp]
theorem range_castAddHom {A : Type*} [AddGroupWithOne A] : (Int.castAddHom A).range = AddSubgroup.zmultiples 1 :=
  by
  ext a
  simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]

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