Theorems · Theorem · linear algebra
IsLocalization.rank_eq
∀ {R : Type uR} (S : Type uS) {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : AddCommGroup N]
[inst_3 : Module R N] [inst_4 : Algebra R S] [inst_5 : Module S N] [IsScalarTower R S N] (p : Submonoid R)
[IsLocalization p S], p ≤ nonZeroDivisors R → Module.rank S N = Module.rank R N- Cited by
- 7 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites30
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
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- Algebrastatement and proof · cited by 11,388
- Set.Elemproof · cited by 7,166
- Algebra.algebraMapproof · cited by 4,706
- IsScalarTowerstatement and proof · cited by 3,896
- Submonoidstatement and proof · cited by 3,086
- Cardinalstatement and proof · cited by 2,598
- Nontrivialproof · cited by 2,416
Cited by7
Results whose statement or proof uses this declaration.
- IsBaseChange.lift_rank_eqproof · cited by 3
- IsBaseChange.lift_rank_eq_of_le_nonZeroDivisorsproof · cited by 3
- IsLocalization.finrank_eqproof · cited by 1
- Algebra.IsAlgebraic.lift_rank_of_isFractionRingproof · cited by 1
- IsFractionRing.rank_right_eqproof · cited by 0
- exists_set_linearIndependent_of_isDomainproof · cited by 0
- rank_quotient_add_rank_of_isDomainproof · cited by 0