mapRangeRingHom_single — Mathlib

English

The mapRangeRingHom sends a basis element (single a b) to the corresponding basis element (single a (f b)).

Русский

MapRangeRingHom отправляет базисный элемент (single a b) в соответствующий базисный элемент (single a (f b)).

LaTeX

$$$ mapRangeRingHom\ M\ f\ (single\ a\ b) = single\ a\ (f b) $$$

Lean4

@[simp]
theorem mapRangeRingHom_single (f : R →+* S) (a : M) (b : R) : mapRangeRingHom M f (single a b) = single a (f b) := by
  classical ext; simp [single_apply, apply_ite f]

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