Theorems · Theorem · commutative algebra
IsArtinianRing.of_finite
∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Module R S] [IsScalarTower R S S] [IsArtinianRing R] [Module.Finite R S], IsArtinianRing S
- Defined in
- Mathlib.RingTheory.Artinian.Module
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Ringstatement and proof · cited by 7,463
- IsScalarTowerstatement and proof · cited by 3,896
- Module.Finitestatement and proof · cited by 1,032
- IsArtinianRingstatement and proof · cited by 98
- isArtinian_of_towerproof · cited by 6
Cited by9
Results whose statement or proof uses this declaration.
- Module.End.isSemisimple_of_squarefree_aeval_eq_zeroproof · cited by 4
- Module.End.IsSemisimple.of_mem_adjoin_pairproof · cited by 3
- Algebra.QuasiFiniteAt.exists_basicOpen_eq_singletonproof · cited by 2
- AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFiniteproof · cited by 2
- Algebra.FormallyEtale.of_formallyUnramified_of_fieldproof · cited by 1
- isDedekindDomainDvr.of_formallyUnramifiedproof · cited by 1
- Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_topproof · cited by 1
- IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosedproof · cited by 0
- Algebra.IsUnramifiedAt.not_minpoly_sq_dvdproof · cited by 0