mapDomain_one — Mathlib

English

mapDomain is compatible with RingHom structure, i.e., it respects addition and multiplication when applied to RingHom arguments.

Русский

mapDomain совместим с кольцевой структурой: сохранение сложения и умножения при применении к RingHom.

LaTeX

$$$ mapDomain\ f \ (x + y) = mapDomain\ f\ x + mapDomain\ f\ y \quad\text{и}\quad mapDomain\ f\ (x \cdot y) = mapDomain\ f\ x \cdot mapDomain\ f\ y $$$

Lean4

@[to_additive (dont_translate := R) (attr := simp) mapDomain_one]
theorem mapDomain_one [One M] [One N] {F : Type*} [FunLike F M N] [OneHomClass F M N] (f : F) :
    mapDomain f (1 : MonoidAlgebra R M) = (1 : MonoidAlgebra R N) := by simp [one_def]

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