smulRight_apply_eq_zero_iff — Mathlib

English

Under NoZeroSMulDivisors S M, f.smulRight x = 0 iff f = 0 or x = 0 (with the standard NoZeroSMulDivisors assumption).

Русский

При условии NoZeroSMulDivisors S M, f.smulRight x = 0 эквивалентно f = 0 или x = 0 (при стандартном предположении NoZeroSMulDivisors).

LaTeX

$$f.smulRight x = 0 \iff f = 0 \lor x = 0$$

Lean4

@[simp]
theorem smulRight_apply_eq_zero_iff {f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] :
    f.smulRight x = 0 ↔ f = 0 ∨ x = 0 := by
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  refine ⟨fun h ↦ Or.inl ?_, fun h ↦ by simp [h.resolve_right hx]⟩
  ext v
  replace h : f v • x = 0 := by simpa only [LinearMap.zero_apply] using LinearMap.congr_fun h v
  rw [smul_eq_zero] at h
  tauto

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