mapRangeAlgHom_single — Mathlib

English

For an algebra hom f: A →ₐ[R] B, an index m ∈ M, and a ∈ A, mapRangeAlgHom M f applied to single m a equals single m (f a).

Русский

Для алгебра-гомоморфизма f: A →ₐ[R] B и элемента single m a: mapRangeAlgHom M f (single m a) = single m (f a).

LaTeX

$$$\\mathrm{mapRangeAlgHom}\\ M f (\\mathrm{single} m a) = \\mathrm{single} m (f a).$$$

Lean4

@[to_additive (attr := simp)]
theorem mapRangeAlgHom_single (f : A →ₐ[R] B) (m : M) (a : A) : mapRangeAlgHom M f (single m a) = single m (f a) := by
  classical ext; simp [single_apply, apply_ite f]

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