Theorems · Theorem · commutative algebra
Module.free_of_flat_of_isLocalRing
∀ {R : Type u_1} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup P] [inst_2 : Module R P] [IsLocalRing R]
[Module.Finite R P] [Module.Flat R P], Module.Free R P[Stacks Tag 00NZ](https://stacks.math.columbia.edu/tag/00NZ)
- Defined in
- Mathlib.RingTheory.LocalRing.Module
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
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
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- TensorProductproof · cited by 2,545
- Module.Basisproof · cited by 1,477
- Module.Finitestatement and proof · cited by 1,032
- Module.Freestatement and proof · cited by 597
- Eq.geproof · cited by 375
- IsLocalRingstatement and proof · cited by 339
- Module.Flatstatement and proof · cited by 279
- IsLocalRing.ResidueFieldproof · cited by 156
Cited by7
Results whose statement or proof uses this declaration.
- Algebra.smoothLocus_eq_compl_support_interproof · cited by 2
- IsLocalRing.minpoly_map_residueproof · cited by 1
- IsLocalRing.finrank_eq_finrank_residueFieldproof · cited by 1
- ModuleCat.projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegularproof · cited by 1
- Module.freeLocus_eq_univproof · cited by 1
- Module.freeLocus_eq_univ_iffproof · cited by 1
- Module.rankAtStalk_piproof · cited by 0