Theorems · Theorem · linear algebra
Finsupp.coe_basisSingleOne
∀ {R : Type u_1} {ι : Type u_3} [inst : Semiring R], ⇑Finsupp.basisSingleOne = fun i => fun₀ | i => 1- Cited by
- 7 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Finsuppstatement · cited by 5,255
- Module.Basisstatement · cited by 1,477
- Finsupp.singlestatement · cited by 943
- Finsupp.basisSingleOnestatement · cited by 16
- Module.Basis.apply_eq_iffproof · cited by 12
Cited by7
Results whose statement or proof uses this declaration.
- Module.Basis.tensorProduct_applyproof · cited by 9
- Module.Basis.baseChange_applyproof · cited by 7
- Algebra.FormallyUnramified.finite_of_freeproof · cited by 7
- Module.Flat.tfae_equational_criterionproof · cited by 2
- Finsupp.lcomapDomain_eq_linearProjOfIsComplproof · cited by 1
- Module.Free.bijective_algebraMap_of_finrank_eq_oneproof · cited by 1
- Module.Basis.tensorProduct_apply'proof · cited by 1