range_neg — Mathlib

English

The range of the negated map equals the range of the map itself: range(-f) = range(f).

Русский

Диапазон отображения после взятия минуса равно диапазону исходного отображения: range(-f) = range(f).

LaTeX

$$$\operatorname{range}(-f) = \operatorname{range} f$$$

Lean4

@[simp]
theorem range_neg {R : Type*} {R₂ : Type*} {M : Type*} {M₂ : Type*} [Semiring R] [Ring R₂] [AddCommMonoid M]
    [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
    LinearMap.range (-f) = LinearMap.range f :=
  by
  change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _
  rw [range_comp, Submodule.map_neg, Submodule.map_id]

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