mapRangeRingHom_apply — Mathlib

English

The value of mapRangeRingHom applied to an element x at basis index m is equal to the image of the coefficient x(m) under f.

Русский

Значение mapRangeRingHom в точке индекса базиса m равно образу коэффициента x(m) под действием f.

LaTeX

$$$mapRangeRingHom\ M f x m = f\bigl(x(m)\bigr)$$$

Lean4

@[simp]
theorem mapRangeRingHom_apply (f : R →+* S) (x : MonoidAlgebra R M) (m : M) : mapRangeRingHom M f x m = f (x m) := by
  classical
  induction x using induction_linear
  · simp
  · simp [*]
  · simp [mapRangeRingHom, single_apply, apply_ite (f := f)]

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