Theorems · Theorem · commutative algebra
Module.Free.exists_basis
∀ (R : Type u) (M : Type v) {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
[self : Module.Free R M], Nonempty ((I : Type v) × Module.Basis I R M)- Defined in
- Mathlib.LinearAlgebra.FreeModule.Basic
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- Module.Free
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Module.Basisstatement · cited by 1,477
- Module.Freestatement and proof · cited by 597
Cited by26
Results whose statement or proof uses this declaration.
- rank_finsuppproof · cited by 4
- rank_tensorProductproof · cited by 4
- Module.free_defproof · cited by 3
- Subalgebra.eq_bot_of_rank_le_oneproof · cited by 3
- Module.Free.exists_setproof · cited by 3
- nonempty_linearEquiv_of_lift_rank_eqproof · cited by 3
- rank_matrix_moduleproof · cited by 3
- Subalgebra.rank_eq_one_iffproof · cited by 3
- Module.finite_of_rank_eq_natproof · cited by 2
- LinearMap.BilinForm.Nondegenerate.ofSeparatingLeftproof · cited by 2
- rank_fun_infiniteproof · cited by 2
- lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rankproof · cited by 2