Theorems · Theorem · linear algebra

Module.Basis.mk_eq_rank

∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] (v : Module.Basis ι R M),
  Cardinal.lift.{v, w} (Cardinal.mk ι) = Cardinal.lift.{w, v} (Module.rank R M)

Defined in: Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Cited by: 10 results in Mathlib
Foundations: Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring AddCommMonoid Module StrongRankCondition

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

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
Cardinalstatement and proof · cited by 2,598
Nontrivialproof · cited by 2,416
Module.Basisstatement and proof · cited by 1,477
Cardinal.mkstatement and proof · cited by 942
Cardinal.liftstatement and proof · cited by 583
Module.rankstatement · cited by 496
StrongRankConditionstatement and proof · cited by 286
nontrivial_of_invariantBasisNumberproof · cited by 18
Cardinal.mk_range_eq_of_injectiveproof · cited by 14

Cited by10

Results whose statement or proof uses this declaration.

Module.rank_selfproof · cited by 17
rank_spanproof · cited by 6
Module.finrank_eq_nat_card_basisproof · cited by 5
lift_rank_mul_lift_rankproof · cited by 4
MvPolynomial.rank_eq_liftproof · cited by 3
rank_prodproof · cited by 2
Module.Basis.nonempty_fintype_index_of_rank_lt_aleph0proof · cited by 2
Algebra.TensorProduct.not_isField_of_transcendentalproof · cited by 1
Module.Basis.mk_eq_rank'proof · cited by 1
MvPolynomial.rank_eqproof · cited by 0