mem_smul_span_iff — Mathlib

English

For v : ι → ℝ, v ∈ (n)^{-1} • L iff ∀ i, n · v_i ∈ range(algebraMap ℤ ℝ).

Русский

Для v : ι → ℝ, v ∈ (n)^{-1} • L тогда и только тогда, когда ∀ i, n · v_i ∈ образ(алгебраMap ℤ → ℝ).

LaTeX

$$$$ v \\in (n : \\mathbb{R})^{-1} \\cdot L \\iff \\forall i,\\ n \\cdot v(i) \\in \\operatorname{range}(\\mathrm{algebraMap} \\ \\mathbb{Z} \\ \\mathbb{R}) $$$$

Lean4

theorem mem_smul_span_iff {v : ι → ℝ} : v ∈ (n : ℝ)⁻¹ • L ↔ ∀ i, n * v i ∈ Set.range (algebraMap ℤ ℝ) :=
  by
  rw [ZSpan.smul _ (inv_ne_zero (NeZero.ne _)), Module.Basis.mem_span_iff_repr_mem]
  simp_rw [Module.Basis.repr_isUnitSMul, Pi.basisFun_repr, Units.smul_def, Units.val_inv_eq_inv_val, IsUnit.unit_spec,
    inv_inv, smul_eq_mul]

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