AffineBasis.tot
∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
[inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P), affineSpan k (Set.range ⇑b) = ⊤- Defined in
- Mathlib.LinearAlgebra.AffineSpace.Basis
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Top.topstatement · cited by 9,680
- Ringstatement and proof · cited by 7,463
- Set.rangestatement · cited by 4,705
- AddTorsorstatement and proof · cited by 1,657
- AffineSubspacestatement · cited by 871
- affineSpanstatement · cited by 417
- AffineBasisstatement and proof · cited by 65
- AffineBasis.tot'proof · cited by 1
Cited by8
Results whose statement or proof uses this declaration.
- AffineBasis.sum_coord_apply_eq_oneproof · cited by 4
- AffineBasis.affineCombination_coord_eq_selfproof · cited by 3
- AffineBasis.nonemptyproof · cited by 2
- AffineBasis.affineSpan_eq_top_of_toMatrix_left_invproof · cited by 1
- AffineBasis.card_eq_finrank_add_oneproof · cited by 1
- AffineBasis.coe_coord_of_subsingleton_eq_oneproof · cited by 1
- AffineBasis.convexHull_eq_nonneg_coordproof · cited by 1
- AffineBasis.interior_convexHullproof · cited by 1