Theorems · Theorem · real analysis
BoxIntegral.unitPartition.mem_smul_span_iff
∀ {ι : Type u_1} {n : ℕ} [NeZero n] [inst : Finite ι] {v : ι → ℝ},
v ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- RingHomstatement · cited by 10,189
- Fintypeproof · cited by 7,736
- Submodulestatement and proof · cited by 7,192
- Algebra.algebraMapstatement and proof · cited by 4,706
- Set.rangestatement and proof · cited by 4,705
- Finitestatement and proof · cited by 3,029
- Submodule.spanstatement · cited by 1,504
- Module.Basisstatement · cited by 1,477
- inv_invproof · cited by 494
Cited by2
Results whose statement or proof uses this declaration.
- BoxIntegral.unitPartition.tag_index_eq_self_of_mem_smul_spanproof · cited by 2
- BoxIntegral.unitPartition.tag_mem_smul_spanproof · cited by 1