English
For a type A with R‑module structure and suitable scalar actions, the range of multiplication by a is the restricted span by a: range(mul R A a) = (span{a}).restrictScalars R.
Русский
Для типа A со структурой модуля над R и подходящими скалярными действиями, образ умножения на a равен ограниченному спану a: range(mul R A a) = (span{a}).restrictScalars R.
LaTeX
$$$ \\operatorname{range}( \\mathrm{LinearMap.mul}\\, R\\, A\\, a) = (\\operatorname{span}\\{a\\}).\\mathrm{restrictScalars}\\, R$$$
Lean4
@[simp]
theorem range_mul (A : Type*) [CommSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : A) :
LinearMap.range (LinearMap.mul R A a) = (Ideal.span { a }).restrictScalars R := by
aesop (add simp Ideal.mem_span_singleton) (add simp dvd_def)
