one_eq_mrange — Mathlib

English

For any additive monoid with one, the unit 1 is the image of the natural numbers under the casting homomorphism into R.

Русский

Для любого аддитивного моноида с единицей 1 является образом натуральных чисел через соответствующий морфизм в R.

LaTeX

$$$(1 : AddSubmonoid R) = AddMonoidHom.mrange (Nat.castAddMonoidHom R)$$$

Lean4

theorem one_eq_mrange : (1 : AddSubmonoid R) = AddMonoidHom.mrange (Nat.castAddMonoidHom R) :=
  rfl

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