restrict_monoidHom — Mathlib

English

Properties of the restricted additive monoid homomorphism ensure homomorphism structure is preserved when restricted to 𝓞_K.

Русский

Свойства ограниченного аддитивного моноид-гомоморфизма обеспечивают сохранение структуры гомоморфизма при ограничении к 𝓞_K.

LaTeX

$$$\\text{restrict\_addMonoidHom}(f,h)$ preserves zero and addition$$

Lean4

/-- Given `f : M →* K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
`M →* 𝓞 K`. -/
def restrict_monoidHom [MulOneClass M] (f : M →* K) (h : ∀ x, IsIntegral ℤ (f x)) : M →* 𝓞 K
    where
  toFun := restrict f h
  map_one' := by simp only [restrict, map_one, mk_one]
  map_mul' x y := by simp only [restrict, map_mul, mk_mul_mk _]

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