Theorems · Theorem · linear algebra
IsBaseChange.finrank_eq
∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {T : Type uT}
[inst_3 : CommRing T] [NoZeroDivisors T] [inst_5 : Algebra R T] [FaithfulSMul R T] {P : Type uP}
[inst_7 : AddCommGroup P] [inst_8 : Module R P] [inst_9 : Module T P] [inst_10 : IsScalarTower R T P] {g : M →ₗ[R] P},
IsBaseChange T g → Module.finrank T P = Module.finrank R M- Cited by
- 1 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- Algebrastatement and proof · cited by 11,388
- LinearMapstatement and proof · cited by 10,215
- IsScalarTowerstatement and proof · cited by 3,896
- Module.finrankstatement · cited by 1,770
- NoZeroDivisorsstatement and proof · cited by 545
- Module.rankproof · cited by 496
- FaithfulSMulstatement and proof · cited by 340
Cited by1
Results whose statement or proof uses this declaration.
- Ideal.finrank_fiber_eq_finrankproof · cited by 1