restrict_addMonoidHom — Mathlib

English

Given an additive monoid hom f: M → K with IsIntegral for all x, there is a corresponding additive monoid hom M → 𝓞_K.

Русский

Дано $f:M\\to K$ как моноид-гомоморфиз, удовлетворяющий IsIntegral для всех x; существует соответствующий моноид-гомоморфизм $M\\to \\mathcal{O}_K$.

LaTeX

$$$\\text{restrict\_addMonoidHom}(f,h): M \\to \\mathcal{O}_K$$$

Lean4

/-- Given `f : M →+ K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
`M →+ 𝓞 K`. -/
def restrict_addMonoidHom [AddZeroClass M] (f : M →+ K) (h : ∀ x, IsIntegral ℤ (f x)) : M →+ 𝓞 K
    where
  toFun := restrict f h
  map_zero' := by simp only [restrict, map_zero, mk_zero]
  map_add' x y := by simp only [restrict, map_add, mk_add_mk _]

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