mk_span_range — Mathlib

English

In the quotient by span(range f), the element f(i) maps to zero for all i.

Русский

В факторкольце по оболочке span(range f) образ элемента f(i) равен нулю для всех i.

LaTeX

$$mk (span (range f)) (f i) = 0$$

Lean4

@[simp]
theorem mk_span_range {ι : Type*} (f : ι → R) [(span (range f)).IsTwoSided] (i : ι) : mk (span (.range f)) (f i) = 0 :=
  by
  rw [Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.subset_span ⟨i, rfl⟩

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