Theorems · Definition · ring theory
IsIsotypic
(R : Type u_2) → (M : Type u) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → Prop
An R-module M is isotypic if all its simple submodules are isomorphic.
- Defined in
- Mathlib.RingTheory.SimpleModule.Isotypic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
- Assumes
- RingAddCommGroupModule
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
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Submoduleproof · cited by 7,192
- IsSimpleModuleproof · cited by 114
- IsIsotypicOfTypeproof · cited by 16
Cited by15
Results whose statement or proof uses this declaration.
- IsIsotypic.linearEquiv_funstatement and proof · cited by 3
- IsIsotypic.isotypicComponentstatement · cited by 2
- IsIsotypicOfType.isIsotypicstatement · cited by 2
- IsSimpleRing.isIsotypicstatement · cited by 2
- isSimpleRing_isArtinianRing_iffstatement and proof · cited by 1
- IsIsotypic.isotypicComponentsstatement · cited by 1
- IsIsotypic.of_injectivestatement and proof · cited by 1
- IsIsotypic.of_selfstatement and proof · cited by 1
- IsIsotypic.submodule_linearEquiv_funstatement and proof · cited by 1
- isIsotypic_submodule_iffstatement and proof · cited by 1
- LinearEquiv.isIsotypic_iffstatement and proof · cited by 0
- IsIsotypic.linearEquiv_finsuppstatement and proof · cited by 0