Theorems · Theorem · linear algebra
rank_eq_zero_iff
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0See rank_zero_iff for a stronger version with IsTorsionFree R M.
- Defined in
- Mathlib.LinearAlgebra.Dimension.Finite
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites35
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Set.Elemproof · cited by 7,166
- Finsuppproof · cited by 5,255
- Cardinalstatement and proof · cited by 2,598
- Nat.cast_oneproof · cited by 2,501
- Nontrivialproof · cited by 2,416
- Finsupp.singleproof · cited by 943
- Cardinal.mkproof · cited by 942
Cited by3
Results whose statement or proof uses this declaration.
- ModularForm.levelOne_neg_weight_rank_zeroproof · cited by 4
- Module.finrank_eq_zero_iffproof · cited by 0
- Submodule.exists_smul_notMem_of_rank_ltproof · cited by 0